Metamath Proof Explorer

Theorem lesubadd

Description: 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

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