Theorem abs3lemd

Description: Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	abscld.1	$$⊢\phi \to A\in ℂ$$
	abssubd.2	$$⊢\phi \to B\in ℂ$$
	abs3difd.3	$$⊢\phi \to C\in ℂ$$
	abs3lemd.4	$$⊢\phi \to D\in ℝ$$
	abs3lemd.5	$$⊢\phi \to \left|A-C\right|<\frac{D}{2}$$
	abs3lemd.6	$$⊢\phi \to \left|C-B\right|<\frac{D}{2}$$
Assertion	abs3lemd	$$⊢\phi \to \left|A-B\right|<D$$

Proof

Step	Hyp	Ref	Expression
1		abscld.1	$$⊢\phi \to A\in ℂ$$
2		abssubd.2	$$⊢\phi \to B\in ℂ$$
3		abs3difd.3	$$⊢\phi \to C\in ℂ$$
4		abs3lemd.4	$$⊢\phi \to D\in ℝ$$
5		abs3lemd.5	$$⊢\phi \to \left|A-C\right|<\frac{D}{2}$$
6		abs3lemd.6	$$⊢\phi \to \left|C-B\right|<\frac{D}{2}$$
7		abs3lem	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(C\in ℂ\wedge D\in ℝ\right)\right)\to \left(\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-B\right|<D\right)$$
8	1 2 3 4 7	syl22anc	$$⊢\phi \to \left(\left(\left|A-C\right|<\frac{D}{2}\wedge \left|C-B\right|<\frac{D}{2}\right)\to \left|A-B\right|<D\right)$$
9	5 6 8	mp2and	$$⊢\phi \to \left|A-B\right|<D$$