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