Metamath Proof Explorer

Theorem abs2dif2

Description: Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Assertion abs2dif2 
|- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 abstri 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( abs ` ( A + -u B ) ) <_ ( ( abs ` A ) + ( abs ` -u B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + -u B ) ) <_ ( ( abs ` A ) + ( abs ` -u B ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + -u B ) ) = ( abs ` ( A - B ) ) )
6 absneg 
 |-  ( B e. CC -> ( abs ` -u B ) = ( abs ` B ) )
7 6 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` -u B ) = ( abs ` B ) )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) + ( abs ` -u B ) ) = ( ( abs ` A ) + ( abs ` B ) ) )
9 3 5 8 3brtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )