Let $x_1, \ldots, x_N \in (0, \infty)$ each be a D5407: Positive real number.

Then \begin{equation} \lim_{p \searrow 0 : p \neq 0} \left( \frac{1}{N} \sum_{n = 1}^N x_n^p \right)^{1/p} = \left( \prod_{n = 1}^N x_n \right)^{1/N} \end{equation}