Metamath Proof Explorer

Theorem sgn0

Description: The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion sgn0 
|- ( sgn ` 0 ) = 0

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 sgnval 
 |-  ( 0 e. RR* -> ( sgn ` 0 ) = if ( 0 = 0 , 0 , if ( 0 < 0 , -u 1 , 1 ) ) )
3 1 2 ax-mp 
 |-  ( sgn ` 0 ) = if ( 0 = 0 , 0 , if ( 0 < 0 , -u 1 , 1 ) )
4 eqid 
 |-  0 = 0
5 4 iftruei 
 |-  if ( 0 = 0 , 0 , if ( 0 < 0 , -u 1 , 1 ) ) = 0
6 3 5 eqtri 
 |-  ( sgn ` 0 ) = 0