Let $x, y \in [0, \infty)$ each be an D4767: Unsigned real number.
Then
| (1) | \begin{equation} x y \leq \left( \frac{x + y}{2} \right)^2 \end{equation} |
| (2) | \begin{equation} x y = \left( \frac{x + y}{2} \right)^2 \quad \iff\quad x = y \end{equation} |