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

Result R4228 on D871: Basic real ordering relation
Subresult of R1904: Isotonicity of finite real summation

Real ordering is compatible with addition

Formulation 0

Let $P = (\mathbb{R}, {\leq})$ be the D1102: Ordered set of real numbers.
Let $x, y, z \in \mathbb{R}$ each be a D993: Real number such that

(i)	\begin{equation} x \leq y \end{equation}

Then \begin{equation} x + z \leq y + z \end{equation}

Proofs

Proof 0

Let $P = (\mathbb{R}, {\leq})$ be the D1102: Ordered set of real numbers.
Let $x, y, z \in \mathbb{R}$ each be a D993: Real number such that

(i)	\begin{equation} x \leq y \end{equation}

Since $x \leq y$, then two cases are possible: either $x = y$ or $x < y$. If $x = y$, then $x + z = y + z$ and thus $x + z \leq y + z$. The case $x < y$ is settled in R4227: Strict real ordering is compatible with addition. $\square$