This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐶 + 𝐴 ) < ( 𝐶 + 𝐵 ) ) )