Metamath Proof Explorer


Theorem abs2difabsi

Description: Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Hypotheses abs2difabsi.1
|- A e. CC
abs2difabsi.2
|- B e. CC
Assertion abs2difabsi
|- ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) )

Proof

Step Hyp Ref Expression
1 abs2difabsi.1
 |-  A e. CC
2 abs2difabsi.2
 |-  B e. CC
3 abs2difabs
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
4 1 2 3 mp2an
 |-  ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) )