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