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 ⊢ 𝐴 ∈ ℂ
abssub.2 ⊢ 𝐵 ∈ ℂ
abs3dif.3 ⊢ 𝐶 ∈ ℂ
abs3lem.4 ⊢ 𝐷 ∈ ℝ
Assertion abs3lemi ( ( ( abs ‘ ( 𝐴 − 𝐶 ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( 𝐶 − 𝐵 ) ) < ( 𝐷 / 2 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < 𝐷 )

Proof

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