Theorem sgn0

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

	Ref	Expression
Assertion	sgn0	$$⊢\mathrm{sgn}\left(0\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		0xr	$$⊢0\in {ℝ}^{*}$$
2		sgnval	$$⊢0\in {ℝ}^{*}\to \mathrm{sgn}\left(0\right)=if\left(0=0,0,if\left(0<0,-1,1\right)\right)$$
3	1 2	ax-mp	$$⊢\mathrm{sgn}\left(0\right)=if\left(0=0,0,if\left(0<0,-1,1\right)\right)$$
4		eqid	$$⊢0=0$$
5	4	iftruei	$$⊢if\left(0=0,0,if\left(0<0,-1,1\right)\right)=0$$
6	3 5	eqtri	$$⊢\mathrm{sgn}\left(0\right)=0$$