Let $x, y : \mathbb{N} \to \mathbb{R}$ each be a
D4685: Real sequence such that
| (i) |
\begin{equation}
\forall \, n \in \mathbb{N} : x_n \leq y_n
\end{equation}
|
| (ii) |
\begin{equation}
\lim_{N \to \infty} \sum_{n = 0}^N x_n
\neq \emptyset \neq
\lim_{N \to \infty} \sum_{n = 0}^N y_n
\end{equation}
|
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$
