Metamath Proof Explorer

Theorem reabssgn

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

Ref Expression
Assertion reabssgn 
|- ( A e. RR -> ( abs ` A ) = ( ( sgn ` A ) x. A ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( A e. RR -> A e. RR* )
2 sgnval 
 |-  ( A e. RR* -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
3 1 2 syl 
 |-  ( A e. RR -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
4 3 oveq1d 
 |-  ( A e. RR -> ( ( sgn ` A ) x. A ) = ( if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) x. A ) )
5 ovif 
 |-  ( if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) x. A ) = if ( A = 0 , ( 0 x. A ) , ( if ( A < 0 , -u 1 , 1 ) x. A ) )
6 ovif 
 |-  ( if ( A < 0 , -u 1 , 1 ) x. A ) = if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) )
7 ifeq2 
 |-  ( ( if ( A < 0 , -u 1 , 1 ) x. A ) = if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) -> if ( A = 0 , ( 0 x. A ) , ( if ( A < 0 , -u 1 , 1 ) x. A ) ) = if ( A = 0 , ( 0 x. A ) , if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) ) )
8 6 7 ax-mp 
 |-  if ( A = 0 , ( 0 x. A ) , ( if ( A < 0 , -u 1 , 1 ) x. A ) ) = if ( A = 0 , ( 0 x. A ) , if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) )
9 5 8 eqtri 
 |-  ( if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) x. A ) = if ( A = 0 , ( 0 x. A ) , if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) )
10 mul02lem2 
 |-  ( A e. RR -> ( 0 x. A ) = 0 )
11 10 adantr 
 |-  ( ( A e. RR /\ A = 0 ) -> ( 0 x. A ) = 0 )
12 simpr 
 |-  ( ( A e. RR /\ A = 0 ) -> A = 0 )
13 12 abs00bd 
 |-  ( ( A e. RR /\ A = 0 ) -> ( abs ` A ) = 0 )
14 11 13 eqtr4d 
 |-  ( ( A e. RR /\ A = 0 ) -> ( 0 x. A ) = ( abs ` A ) )
15 recn 
 |-  ( A e. RR -> A e. CC )
16 15 mulm1d 
 |-  ( A e. RR -> ( -u 1 x. A ) = -u A )
17 15 mulid2d 
 |-  ( A e. RR -> ( 1 x. A ) = A )
18 16 17 ifeq12d 
 |-  ( A e. RR -> if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) = if ( A < 0 , -u A , A ) )
19 reabsifneg 
 |-  ( A e. RR -> ( abs ` A ) = if ( A < 0 , -u A , A ) )
20 18 19 eqtr4d 
 |-  ( A e. RR -> if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) = ( abs ` A ) )
21 20 adantr 
 |-  ( ( A e. RR /\ -. A = 0 ) -> if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) = ( abs ` A ) )
22 14 21 ifeqda 
 |-  ( A e. RR -> if ( A = 0 , ( 0 x. A ) , if ( A < 0 , ( -u 1 x. A ) , ( 1 x. A ) ) ) = ( abs ` A ) )
23 9 22 syl5eq 
 |-  ( A e. RR -> ( if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) x. A ) = ( abs ` A ) )
24 4 23 eqtr2d 
 |-  ( A e. RR -> ( abs ` A ) = ( ( sgn ` A ) x. A ) )