Metamath Proof Explorer

Theorem reabsifpos

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

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
3 1 2 mpan 
 |-  ( A e. RR -> ( 0 < A -> 0 <_ A ) )
4 3 imdistani 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. RR /\ 0 <_ A ) )
5 absid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
6 4 5 syl 
 |-  ( ( A e. RR /\ 0 < A ) -> ( abs ` A ) = A )
7 6 eqcomd 
 |-  ( ( A e. RR /\ 0 < A ) -> A = ( abs ` A ) )
8 id 
 |-  ( A e. RR -> A e. RR )
9 0red 
 |-  ( A e. RR -> 0 e. RR )
10 8 9 lenltd 
 |-  ( A e. RR -> ( A <_ 0 <-> -. 0 < A ) )
11 10 pm5.32i 
 |-  ( ( A e. RR /\ A <_ 0 ) <-> ( A e. RR /\ -. 0 < A ) )
12 absnid 
 |-  ( ( A e. RR /\ A <_ 0 ) -> ( abs ` A ) = -u A )
13 11 12 sylbir 
 |-  ( ( A e. RR /\ -. 0 < A ) -> ( abs ` A ) = -u A )
14 13 eqcomd 
 |-  ( ( A e. RR /\ -. 0 < A ) -> -u A = ( abs ` A ) )
15 7 14 ifeqda 
 |-  ( A e. RR -> if ( 0 < A , A , -u A ) = ( abs ` A ) )
16 15 eqcomd 
 |-  ( A e. RR -> ( abs ` A ) = if ( 0 < A , A , -u A ) )