Metamath Proof Explorer

Theorem ltadd1

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

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

Proof

Step Hyp Ref Expression
1 ltadd2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ C + A < C + B
2 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
3 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
4 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
5 4 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℂ
6 3 5 addcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A = A + C
7 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
8 7 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
9 3 8 addcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + B = B + C
10 6 9 breq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + A < C + B ↔ A + C < B + C
11 1 10 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < B ↔ A + C < B + C