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 ‘ ( 𝐴𝐵 ) ) < 𝐷 )