This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abs3lemi

Description: Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypotheses absvalsqi.1 ⊢ A ∈ ℂ
abssub.2 ⊢ B ∈ ℂ
abs3dif.3 ⊢ C ∈ ℂ
abs3lem.4 ⊢ D ∈ ℝ
Assertion abs3lemi ⊢ A − C < D 2 ∧ C − B < D 2 → A − B < D

Proof

Step Hyp Ref Expression
1 absvalsqi.1 ⊢ A ∈ ℂ
2 abssub.2 ⊢ B ∈ ℂ
3 abs3dif.3 ⊢ C ∈ ℂ
4 abs3lem.4 ⊢ D ∈ ℝ
5 1 2 3 abs3difi ⊢ A − B ≤ A − C + C − B
6 1 3 subcli ⊢ A − C ∈ ℂ
7 6 abscli ⊢ A − C ∈ ℝ
8 3 2 subcli ⊢ C − B ∈ ℂ
9 8 abscli ⊢ C − B ∈ ℝ
10 4 rehalfcli ⊢ D 2 ∈ ℝ
11 7 9 10 10 lt2addi ⊢ A − C < D 2 ∧ C − B < D 2 → A − C + C − B < D 2 + D 2
12 1 2 subcli ⊢ A − B ∈ ℂ
13 12 abscli ⊢ A − B ∈ ℝ
14 7 9 readdcli ⊢ A − C + C − B ∈ ℝ
15 10 10 readdcli ⊢ D 2 + D 2 ∈ ℝ
16 13 14 15 lelttri ⊢ A − B ≤ A − C + C − B ∧ A − C + C − B < D 2 + D 2 → A − B < D 2 + D 2
17 5 11 16 sylancr ⊢ A − C < D 2 ∧ C − B < D 2 → A − B < D 2 + D 2
18 10 recni ⊢ D 2 ∈ ℂ
19 18 2timesi ⊢ 2 ⁢ D 2 = D 2 + D 2
20 4 recni ⊢ D ∈ ℂ
21 2cn ⊢ 2 ∈ ℂ
22 2ne0 ⊢ 2 ≠ 0
23 20 21 22 divcan2i ⊢ 2 ⁢ D 2 = D
24 19 23 eqtr3i ⊢ D 2 + D 2 = D
25 17 24 breqtrdi ⊢ A − C < D 2 ∧ C − B < D 2 → A − B < D