Theorem sgnn

Description: The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		sgnval	$$⊢A\in {ℝ}^{*}\to \mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to \mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4		xrltne	$$⊢\left(A\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge A<0\right)\to 0\ne A$$
5	3 4	mp3an2	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to 0\ne A$$
6		nesym	$$⊢0\ne A\leftrightarrow \neg A=0$$
7	5 6	sylib	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to \neg A=0$$
8	7	iffalsed	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to if\left(A=0,0,if\left(A<0,-1,1\right)\right)=if\left(A<0,-1,1\right)$$
9		iftrue	$$⊢A<0\to if\left(A<0,-1,1\right)=-1$$
10	9	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to if\left(A<0,-1,1\right)=-1$$
11	2 8 10	3eqtrd	$$⊢\left(A\in {ℝ}^{*}\wedge A<0\right)\to \mathrm{sgn}\left(A\right)=-1$$