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