Metamath Proof Explorer

Theorem abs2difabs

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

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

Proof

Step Hyp Ref Expression
1 abs2dif 
 |-  ( ( B e. CC /\ A e. CC ) -> ( ( abs ` B ) - ( abs ` A ) ) <_ ( abs ` ( B - A ) ) )
2 1 ancoms 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` B ) - ( abs ` A ) ) <_ ( abs ` ( B - A ) ) )
3 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
4 3 recnd 
 |-  ( A e. CC -> ( abs ` A ) e. CC )
5 abscl 
 |-  ( B e. CC -> ( abs ` B ) e. RR )
6 5 recnd 
 |-  ( B e. CC -> ( abs ` B ) e. CC )
7 negsubdi2 
 |-  ( ( ( abs ` A ) e. CC /\ ( abs ` B ) e. CC ) -> -u ( ( abs ` A ) - ( abs ` B ) ) = ( ( abs ` B ) - ( abs ` A ) ) )
8 4 6 7 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( ( abs ` A ) - ( abs ` B ) ) = ( ( abs ` B ) - ( abs ` A ) ) )
9 abssub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
10 2 8 9 3brtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
11 abs2dif 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
12 resubcl 
 |-  ( ( ( abs ` A ) e. RR /\ ( abs ` B ) e. RR ) -> ( ( abs ` A ) - ( abs ` B ) ) e. RR )
13 3 5 12 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` A ) - ( abs ` B ) ) e. RR )
14 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
15 abscl 
 |-  ( ( A - B ) e. CC -> ( abs ` ( A - B ) ) e. RR )
16 14 15 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) e. RR )
17 absle 
 |-  ( ( ( ( abs ` A ) - ( abs ` B ) ) e. RR /\ ( abs ` ( A - B ) ) e. RR ) -> ( ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) <-> ( -u ( abs ` ( A - B ) ) <_ ( ( abs ` A ) - ( abs ` B ) ) /\ ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) ) ) )
18 13 16 17 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) <-> ( -u ( abs ` ( A - B ) ) <_ ( ( abs ` A ) - ( abs ` B ) ) /\ ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) ) ) )
19 lenegcon1 
 |-  ( ( ( ( abs ` A ) - ( abs ` B ) ) e. RR /\ ( abs ` ( A - B ) ) e. RR ) -> ( -u ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) <-> -u ( abs ` ( A - B ) ) <_ ( ( abs ` A ) - ( abs ` B ) ) ) )
20 13 16 19 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) <-> -u ( abs ` ( A - B ) ) <_ ( ( abs ` A ) - ( abs ` B ) ) ) )
21 20 anbi1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( -u ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) /\ ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) ) <-> ( -u ( abs ` ( A - B ) ) <_ ( ( abs ` A ) - ( abs ` B ) ) /\ ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) ) ) )
22 18 21 bitr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) <-> ( -u ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) /\ ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) ) ) )
23 10 11 22 mpbir2and 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )