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