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