Theorem absnpncan2d

Description: Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	absnpncan2d.a	$$⊢\phi \to A\in ℂ$$
	absnpncan2d.b	$$⊢\phi \to B\in ℂ$$
	absnpncan2d.c	$$⊢\phi \to C\in ℂ$$
	absnpncan2d.d	$$⊢\phi \to D\in ℂ$$
Assertion	absnpncan2d	$$⊢\phi \to \left|A-D\right|\le \left|A-B\right|+\left|B-C\right|+\left|C-D\right|$$

Proof

Step	Hyp	Ref	Expression
1		absnpncan2d.a	$$⊢\phi \to A\in ℂ$$
2		absnpncan2d.b	$$⊢\phi \to B\in ℂ$$
3		absnpncan2d.c	$$⊢\phi \to C\in ℂ$$
4		absnpncan2d.d	$$⊢\phi \to D\in ℂ$$
5	1 4	subcld	$$⊢\phi \to A-D\in ℂ$$
6	5	abscld	$$⊢\phi \to \left|A-D\right|\in ℝ$$
7	1 3	subcld	$$⊢\phi \to A-C\in ℂ$$
8	7	abscld	$$⊢\phi \to \left|A-C\right|\in ℝ$$
9	3 4	subcld	$$⊢\phi \to C-D\in ℂ$$
10	9	abscld	$$⊢\phi \to \left|C-D\right|\in ℝ$$
11	8 10	readdcld	$$⊢\phi \to \left|A-C\right|+\left|C-D\right|\in ℝ$$
12	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
13	12	abscld	$$⊢\phi \to \left|A-B\right|\in ℝ$$
14	2 3	subcld	$$⊢\phi \to B-C\in ℂ$$
15	14	abscld	$$⊢\phi \to \left|B-C\right|\in ℝ$$
16	13 15	readdcld	$$⊢\phi \to \left|A-B\right|+\left|B-C\right|\in ℝ$$
17	16 10	readdcld	$$⊢\phi \to \left|A-B\right|+\left|B-C\right|+\left|C-D\right|\in ℝ$$
18	1 4 3	abs3difd	$$⊢\phi \to \left|A-D\right|\le \left|A-C\right|+\left|C-D\right|$$
19	1 3 2	abs3difd	$$⊢\phi \to \left|A-C\right|\le \left|A-B\right|+\left|B-C\right|$$
20	8 16 10 19	leadd1dd	$$⊢\phi \to \left|A-C\right|+\left|C-D\right|\le \left|A-B\right|+\left|B-C\right|+\left|C-D\right|$$
21	6 11 17 18 20	letrd	$$⊢\phi \to \left|A-D\right|\le \left|A-B\right|+\left|B-C\right|+\left|C-D\right|$$