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 ) ) |
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 ) ) |