ThmDex – An index of mathematical definitions, results, and conjectures.
Isotonicity of finite real summation

Let $x_1, y_1, \dots, x_N, y_N \in \mathbb{R}$ each be a D993: Real number such that
 (i) $$x_1 \leq y_1, \quad \dots, \quad x_N \leq y_N$$
Then $$\sum_{n = 1}^N x_n \leq \sum_{n = 1}^N y_n$$

Let $x_1, \dots, x_N \in \mathbb{R}$ and $y_1, \dots, y_N \in \mathbb{R}$ each be a D4685: Real sequence.
Then $$x \leq y \quad \implies \quad \sum_{n = 1}^N x_n \leq \sum_{n = 1}^N y_n$$
Subresults
 ▶ R4228: Real ordering is compatible with addition
Proofs
Proof 0
Let $x_1, \dots, x_N \in \mathbb{R}$ and $y_1, \dots, y_N \in \mathbb{R}$ each be a D4685: Real sequence.
Applying R4228: Real ordering is compatible with addition repeatedly, we have $$\begin{split} \sum_{n = 1}^N x_n & = x_1 + x_2 + x_3 + \cdots + x_{N - 2} + x_{N - 1} + x_N \\ & \leq y_1 + x_2 + x_3 + \cdots + x_{N - 2} + x_{N - 1} + x_N \\ & \leq y_1 + y_2 + x_3 + \cdots + x_{N - 2} + x_{N - 1} + x_N \\ & \leq y_1 + y_2 + y_3 + \cdots + x_{N - 2} + x_{N - 1} + x_N \\ & \; \; \vdots \\ & \leq y_1 + y_2 + y_3 + \cdots + y_{N - 2} + x_{N - 1} + x_N \\ & \leq y_1 + y_2 + y_3 + \cdots + x_{N - 2} + y_{N - 1} + x_N \\ & \leq y_1 + y_2 + y_3 + \cdots + x_{N - 2} + x_{N - 1} + y_N = \sum_{n = 1}^N y_n \end{split}$$