Metamath Proof Explorer

Theorem ltadd2

Description: Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltadd2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B↔C+A<C+B

Proof

Step Hyp Ref Expression
1 axltadd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B→C+A<C+B
2 oveq2 ⊢A=B→C+A=C+B
3 2 a1i ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A=B→C+A=C+B
4 axltadd ⊢B∈ℝ∧A∈ℝ∧C∈ℝ→B<A→C+B<C+A
5 4 3com12 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<A→C+B<C+A
6 3 5 orim12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A=B∨B<A→C+A=C+B∨C+B<C+A
7 6 con3d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→¬C+A=C+B∨C+B<C+A→¬A=B∨B<A
8 simp3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℝ
9 simp1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ
10 8 9 readdcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A∈ℝ
11 simp2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℝ
12 8 11 readdcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+B∈ℝ
13 axlttri ⊢C+A∈ℝ∧C+B∈ℝ→C+A<C+B↔¬C+A=C+B∨C+B<C+A
14 10 12 13 syl2anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A<C+B↔¬C+A=C+B∨C+B<C+A
15 axlttri ⊢A∈ℝ∧B∈ℝ→A<B↔¬A=B∨B<A
16 9 11 15 syl2anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B↔¬A=B∨B<A
17 7 14 16 3imtr4d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A<C+B→A<B
18 1 17 impbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A<B↔C+A<C+B