Metamath Proof Explorer

Theorem reabsifnneg

Description: Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024)

Ref Expression
Assertion reabsifnneg 
|- ( A e. RR -> ( abs ` A ) = if ( 0 <_ A , A , -u A ) )

Proof

Step Hyp Ref Expression
1 absid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
2 1 eqcomd 
 |-  ( ( A e. RR /\ 0 <_ A ) -> A = ( abs ` A ) )
3 0re 
 |-  0 e. RR
4 ltnle 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 <-> -. 0 <_ A ) )
5 ltle 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 -> A <_ 0 ) )
6 4 5 sylbird 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( -. 0 <_ A -> A <_ 0 ) )
7 3 6 mpan2 
 |-  ( A e. RR -> ( -. 0 <_ A -> A <_ 0 ) )
8 7 imdistani 
 |-  ( ( A e. RR /\ -. 0 <_ A ) -> ( A e. RR /\ A <_ 0 ) )
9 absnid 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
10 8 9 syl 
 |-  ( ( A e. RR /\ -. 0 <_ A ) -> ( abs ` A ) = -u A )
11 10 eqcomd 
 |-  ( ( A e. RR /\ -. 0 <_ A ) -> -u A = ( abs ` A ) )
12 2 11 ifeqda 
 |-  ( A e. RR -> if ( 0 <_ A , A , -u A ) = ( abs ` A ) )
13 12 eqcomd 
 |-  ( A e. RR -> ( abs ` A ) = if ( 0 <_ A , A , -u A ) )