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