Theorem axltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-ltadd with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

	Ref	Expression
Assertion	axltadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-pre-ltadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 → ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
2		ltxrlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) )
3	2	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) )
4		readdcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 + 𝐴 ) ∈ ℝ )
5		readdcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
6		ltxrlt	⊢ ( ( ( 𝐶 + 𝐴 ) ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
7	4 5 6	syl2an	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
8	7	3impdi	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
9	8	3coml	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ↔ ( 𝐶 + 𝐴 ) <ℝ ( 𝐶 + 𝐵 ) ) )
10	1 3 9	3imtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )