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