Metamath Proof Explorer

Theorem sgnval

Description: Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion sgnval 
|- ( A e. RR* -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = A -> ( x = 0 <-> A = 0 ) )
2 breq1 
 |-  ( x = A -> ( x < 0 <-> A < 0 ) )
3 2 ifbid 
 |-  ( x = A -> if ( x < 0 , -u 1 , 1 ) = if ( A < 0 , -u 1 , 1 ) )
4 1 3 ifbieq2d 
 |-  ( x = A -> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )
5 df-sgn 
 |-  sgn = ( x e. RR* |-> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) )
6 c0ex 
 |-  0 e. _V
7 negex 
 |-  -u 1 e. _V
8 1ex 
 |-  1 e. _V
9 7 8 ifex 
 |-  if ( A < 0 , -u 1 , 1 ) e. _V
10 6 9 ifex 
 |-  if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) e. _V
11 4 5 10 fvmpt 
 |-  ( A e. RR* -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) )