Metamath Proof Explorer

Theorem absdifle

Description: The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007)

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

Proof

Step Hyp Ref Expression
1 resubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ∈ ℝ
2 absle ⊢ A − B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ − C ≤ A − B ∧ A − B ≤ C
3 1 2 stoic3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ − C ≤ A − B ∧ A − B ≤ C
4 renegcl ⊢ C ∈ ℝ → − C ∈ ℝ
5 leaddsub2 ⊢ B ∈ ℝ ∧ − C ∈ ℝ ∧ A ∈ ℝ → B + − C ≤ A ↔ − C ≤ A − B
6 4 5 syl3an2 ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → B + − C ≤ A ↔ − C ≤ A − B
7 6 3comr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + − C ≤ A ↔ − C ≤ A − B
8 recn ⊢ B ∈ ℝ → B ∈ ℂ
9 recn ⊢ C ∈ ℝ → C ∈ ℂ
10 negsub ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + − C = B − C
11 8 9 10 syl2an ⊢ B ∈ ℝ ∧ C ∈ ℝ → B + − C = B − C
12 11 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + − C = B − C
13 12 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B + − C ≤ A ↔ B − C ≤ A
14 7 13 bitr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → − C ≤ A − B ↔ B − C ≤ A
15 lesubadd2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ A ≤ B + C
16 14 15 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → − C ≤ A − B ∧ A − B ≤ C ↔ B − C ≤ A ∧ A ≤ B + C
17 3 16 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ≤ C ↔ B − C ≤ A ∧ A ≤ B + C