ThmDex – An index of mathematical definitions, results, and conjectures.
P3214
Applying R3500: Homomorphism property of the standard natural real exponential function, we have \begin{equation} \begin{split} \prod_{n = 1}^N x_n = \prod_{n = 1}^N e^{-2^{-n}} = \exp \left( \sum_{n = 1}^N - 2^{-n} \right) = \exp \left( - \sum_{n = 1}^N \left( \frac{1}{2} \right)^n \right) \end{split} \end{equation} Result R3367: Characterisation of convergence of geometric basic real series shows that $\sum_{n = 1}^N ( 1 / 2 )^n \to 1$ as $N \to \infty$. Using result R5167: Standard natural real exponential function is sequentially continuous, we then have \begin{equation} \begin{split} \lim_{N \to \infty} \prod_{n = 1}^N x_n = \lim_{N \to \infty} \exp \left( - \sum_{n = 1}^N \left( \frac{1}{2} \right)^n \right) = \exp \left( - \lim_{N \to \infty} \sum_{n = 1}^N \left( \frac{1}{2} \right)^n \right) = \exp \left( - 1 \right) \end{split} \end{equation} $\square$