Metamath Proof Explorer


Theorem abs3difi

Description: Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypotheses absvalsqi.1
|- A e. CC
abssub.2
|- B e. CC
abs3dif.3
|- C e. CC
Assertion abs3difi
|- ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1
 |-  A e. CC
2 abssub.2
 |-  B e. CC
3 abs3dif.3
 |-  C e. CC
4 abs3dif
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
5 1 2 3 4 mp3an
 |-  ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) )