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	|- ( ph -> A e. CC )
	absnpncan2d.b	|- ( ph -> B e. CC )
	absnpncan2d.c	|- ( ph -> C e. CC )
	absnpncan2d.d	|- ( ph -> D e. CC )
Assertion	absnpncan2d	|- ( ph -> ( abs ` ( A - D ) ) <_ ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		absnpncan2d.a	|- ( ph -> A e. CC )
2		absnpncan2d.b	|- ( ph -> B e. CC )
3		absnpncan2d.c	|- ( ph -> C e. CC )
4		absnpncan2d.d	|- ( ph -> D e. CC )
5	1 4	subcld	|- ( ph -> ( A - D ) e. CC )
6	5	abscld	|- ( ph -> ( abs ` ( A - D ) ) e. RR )
7	1 3	subcld	|- ( ph -> ( A - C ) e. CC )
8	7	abscld	|- ( ph -> ( abs ` ( A - C ) ) e. RR )
9	3 4	subcld	|- ( ph -> ( C - D ) e. CC )
10	9	abscld	|- ( ph -> ( abs ` ( C - D ) ) e. RR )
11	8 10	readdcld	|- ( ph -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - D ) ) ) e. RR )
12	1 2	subcld	|- ( ph -> ( A - B ) e. CC )
13	12	abscld	|- ( ph -> ( abs ` ( A - B ) ) e. RR )
14	2 3	subcld	|- ( ph -> ( B - C ) e. CC )
15	14	abscld	|- ( ph -> ( abs ` ( B - C ) ) e. RR )
16	13 15	readdcld	|- ( ph -> ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) e. RR )
17	16 10	readdcld	|- ( ph -> ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) e. RR )
18	1 4 3	abs3difd	|- ( ph -> ( abs ` ( A - D ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - D ) ) ) )
19	1 3 2	abs3difd	|- ( ph -> ( abs ` ( A - C ) ) <_ ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) )
20	8 16 10 19	leadd1dd	|- ( ph -> ( ( abs ` ( A - C ) ) + ( abs ` ( C - D ) ) ) <_ ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) )
21	6 11 17 18 20	letrd	|- ( ph -> ( abs ` ( A - D ) ) <_ ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) )