This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absnpncan3d

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

Ref Expression
Hypotheses absnpncan3d.a 
|- ( ph -> A e. CC )
absnpncan3d.b 
|- ( ph -> B e. CC )
absnpncan3d.c 
|- ( ph -> C e. CC )
absnpncan3d.d 
|- ( ph -> D e. CC )
absnpncan3d.e 
|- ( ph -> E e. CC )
Assertion absnpncan3d 
|- ( ph -> ( abs ` ( A - E ) ) <_ ( ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) + ( abs ` ( D - E ) ) ) )

Proof

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