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