Metamath Proof Explorer

Theorem lesub1

Description: Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

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