Theorem sgnval

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

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

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=A\to \left(x=0\leftrightarrow A=0\right)$$
2		breq1	$$⊢x=A\to \left(x<0\leftrightarrow A<0\right)$$
3	2	ifbid	$$⊢x=A\to if\left(x<0,-1,1\right)=if\left(A<0,-1,1\right)$$
4	1 3	ifbieq2d	$$⊢x=A\to if\left(x=0,0,if\left(x<0,-1,1\right)\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
5		df-sgn	$$⊢\mathrm{sgn}=\left(x\in {ℝ}^{*}⟼if\left(x=0,0,if\left(x<0,-1,1\right)\right)\right)$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7		negex	$$⊢-1\in \mathrm{V}$$
8		1ex	$$⊢1\in \mathrm{V}$$
9	7 8	ifex	$$⊢if\left(A<0,-1,1\right)\in \mathrm{V}$$
10	6 9	ifex	$$⊢if\left(A=0,0,if\left(A<0,-1,1\right)\right)\in \mathrm{V}$$
11	4 5 10	fvmpt	$$⊢A\in {ℝ}^{*}\to \mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$