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