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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B → C + A < C + B

Proof

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