ThmDex – An index of mathematical definitions, results, and conjectures.
P2190
Consider two sequences $S, T : \mathbb{N} \to \mathbb{R}$ such that $S_N : = \sum_{n = 0}^N x_n$ and $T_N : = \sum_{n = 0}^N y_n$. Since $x \leq y$, then result R1904: Isotonicity of finite real summation guarantees that \begin{equation} S_N = \sum_{n = 0}^N x_n \leq \sum_{n = 0}^N y_n = T_N \end{equation} for every $N \in \mathbb{N}$. Since both series are convergent, then both sequences $S$ and $T$ are convergent. Result R1906: Isotonicity of limits of real sequences therefore implies \begin{equation*} \lim_{N \to \infty} \sum_{n = 0}^N x_n = \lim_{N \to \infty} S_N \leq \lim_{N \to \infty} T_N = \lim_{N \to \infty} \sum_{n = 0}^N y_n \end{equation*} which is the desired outcome. $\square$