Definition df-sgn

Description: Signum function. We do not call it "sign", which is homophonic with "sine" ( df-sin ). Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4 . We define this over RR* ( df-xr ) instead of RR so that it can accept +oo and -oo . Note that df-psgn defines the sign of a permutation, which is different. Value shown in sgnval . (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	df-sgn	$$⊢\mathrm{sgn}=\left(x\in {ℝ}^{*}⟼if\left(x=0,0,if\left(x<0,-1,1\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgn	$$class\mathrm{sgn}$$
1		vx	$$setvarx$$
2		cxr	$$class{ℝ}^{*}$$
3	1	cv	$$setvarx$$
4		cc0	$$class0$$
5	3 4	wceq	$$wffx=0$$
6		clt	$$class<$$
7	3 4 6	wbr	$$wffx<0$$
8		c1	$$class1$$
9	8	cneg	$$class-1$$
10	7 9 8	cif	$$classif\left(x<0,-1,1\right)$$
11	5 4 10	cif	$$classif\left(x=0,0,if\left(x<0,-1,1\right)\right)$$
12	1 2 11	cmpt	$$class\left(x\in {ℝ}^{*}⟼if\left(x=0,0,if\left(x<0,-1,1\right)\right)\right)$$
13	0 12	wceq	$$wff\mathrm{sgn}=\left(x\in {ℝ}^{*}⟼if\left(x=0,0,if\left(x<0,-1,1\right)\right)\right)$$