Metamath Proof Explorer

Theorem lesubadd2

Description: 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999)

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

Proof

Step Hyp Ref Expression
1 lesubadd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ A ≤ C + B
2 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
3 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
4 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
5 4 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℂ
6 3 5 addcomd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + C = C + B
7 6 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ≤ B + C ↔ A ≤ C + B
8 1 7 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ A ≤ B + C