ThmDex – An index of mathematical definitions, results, and conjectures.

Result R1904 on D606: Real addition operation
Subresult of R2933: Isotonicity of countably infinite real summation

Isotonicity of finite real summation

Formulation 0

Let

$x_1, y_1, \dots, x_N, y_N \in \mathbb{R}$ each be a D993: Real number such that

(i)	$\begin{equation} x_1 \leq y_1, \quad \dots, \quad x_N \leq y_N \end{equation}$

Then

$\begin{equation} \sum_{n = 1}^N x_n \leq \sum_{n = 1}^N y_n \end{equation}$

Formulation 1

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

$\begin{equation} x \leq y \quad \implies \quad \sum_{n = 1}^N x_n \leq \sum_{n = 1}^N y_n \end{equation}$

Also known as

Monotonicity of finite real addition

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{equation} \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} \end{equation}$