Metamath Proof Explorer

Theorem leadd2

Description: Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999)

Ref Expression
Assertion leadd2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔C+A≤C+B

Proof

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