Metamath Proof Explorer

Theorem absdiflt

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

Ref Expression
Assertion absdiflt ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B < C ↔ B − C < A ∧ A < B + C

Proof

Step Hyp Ref Expression
1 resubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ∈ ℝ
2 abslt ⊢ 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 ltaddsub2 ⊢ 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 ltsubadd2 ⊢ 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