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 ∈ ℝ*
2		sgnval	⊢ ( 0 ∈ ℝ* → ( sgn ‘ 0 ) = if ( 0 = 0 , 0 , if ( 0 < 0 , - 1 , 1 ) ) )
3	1 2	ax-mp	⊢ ( sgn ‘ 0 ) = if ( 0 = 0 , 0 , if ( 0 < 0 , - 1 , 1 ) )
4		eqid	⊢ 0 = 0
5	4	iftruei	⊢ if ( 0 = 0 , 0 , if ( 0 < 0 , - 1 , 1 ) ) = 0
6	3 5	eqtri	⊢ ( sgn ‘ 0 ) = 0