Metamath Proof Explorer

Theorem abssuble0

Description: Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008)

Ref Expression
Assertion abssuble0 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 abssub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
5 4 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
6 abssubge0 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( B - A ) ) = ( B - A ) )
7 5 6 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( abs ` ( A - B ) ) = ( B - A ) )