Metamath Proof Explorer

Theorem lesub2

Description: Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 leadd2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔C+A≤C+B
2 simp3 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℝ
3 simp1 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℝ
4 2 3 readdcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A∈ℝ
5 simp2 ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℝ
6 lesubadd ⊢C+A∈ℝ∧B∈ℝ∧C∈ℝ→C+A-B≤C↔C+A≤C+B
7 4 5 2 6 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A-B≤C↔C+A≤C+B
8 2 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C∈ℂ
9 3 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A∈ℂ
10 5 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B∈ℂ
11 8 9 10 addsubd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A-B=C-B+A
12 11 breq1d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C+A-B≤C↔C-B+A≤C
13 1 7 12 3bitr2d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔C-B+A≤C
14 2 5 resubcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C−B∈ℝ
15 leaddsub ⊢C−B∈ℝ∧A∈ℝ∧C∈ℝ→C-B+A≤C↔C−B≤C−A
16 14 3 2 15 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C-B+A≤C↔C−B≤C−A
17 13 16 bitrd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→A≤B↔C−B≤C−A