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