Let $x_1, \ldots, x_N \in [0, \infty)$ each be an D4767: Unsigned real number.
Then
| (1) | \begin{equation} \prod_{n = 1}^N x_n \leq \left( \frac{1}{N} \sum_{n = 1}^N x_n \right)^N \end{equation} |
| (2) | \begin{equation} \prod_{n = 1}^N x_n = \left( \frac{1}{N} \sum_{n = 1}^N x_n \right)^N \quad \iff \quad x_1 = x_2 = \cdots = x_N \end{equation} |