Theorem abs3lemi

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

	Ref	Expression
Hypotheses	absvalsqi.1	$$⊢A\in ℂ$$
	abssub.2	$$⊢B\in ℂ$$
	abs3dif.3	$$⊢C\in ℂ$$
	abs3lem.4	$$⊢D\in ℝ$$
Assertion	abs3lemi	$$⊢\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-B\right|<D$$

Proof

Step	Hyp	Ref	Expression
1		absvalsqi.1	$$⊢A\in ℂ$$
2		abssub.2	$$⊢B\in ℂ$$
3		abs3dif.3	$$⊢C\in ℂ$$
4		abs3lem.4	$$⊢D\in ℝ$$
5	1 2 3	abs3difi	$$⊢\left|A-B\right|\le \left|A-C\right|+\left|C-B\right|$$
6	1 3	subcli	$$⊢A-C\in ℂ$$
7	6	abscli	$$⊢\left|A-C\right|\in ℝ$$
8	3 2	subcli	$$⊢C-B\in ℂ$$
9	8	abscli	$$⊢\left|C-B\right|\in ℝ$$
10	4	rehalfcli	$$⊢\frac{D}{2}\in ℝ$$
11	7 9 10 10	lt2addi	$$⊢\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-C\right|+\left|C-B\right|<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
12	1 2	subcli	$$⊢A-B\in ℂ$$
13	12	abscli	$$⊢\left|A-B\right|\in ℝ$$
14	7 9	readdcli	$$⊢\left|A-C\right|+\left|C-B\right|\in ℝ$$
15	10 10	readdcli	$$⊢\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)\in ℝ$$
16	13 14 15	lelttri	$$⊢\left(\left|A-B\right|\le \left|A-C\right|+\left|C-B\right|\wedge \left|A-C\right|+\left|C-B\right|<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)\right)\to \left|A-B\right|<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
17	5 11 16	sylancr	$$⊢\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-B\right|<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
18	10	recni	$$⊢\frac{D}{2}\in ℂ$$
19	18	2timesi	$$⊢2\left(\frac{D}{2}\right)=\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
20	4	recni	$$⊢D\in ℂ$$
21		2cn	$$⊢2\in ℂ$$
22		2ne0	$$⊢2\ne 0$$
23	20 21 22	divcan2i	$$⊢2\left(\frac{D}{2}\right)=D$$
24	19 23	eqtr3i	$$⊢\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)=D$$
25	17 24	breqtrdi	$$⊢\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-B\right|<D$$