Theorem sgnneg

Description: Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018)

	Ref	Expression
Assertion	sgnneg	$$⊢A\in ℝ\to \mathrm{sgn}\left(-A\right)=-\mathrm{sgn}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2	1	negeq0d	$$⊢A\in ℝ\to \left(A=0\leftrightarrow -A=0\right)$$
3	2	bicomd	$$⊢A\in ℝ\to \left(-A=0\leftrightarrow A=0\right)$$
4		eqidd	$$⊢\left(A\in ℝ\wedge -A=0\right)\to 0=0$$
5	3	necon3bbid	$$⊢A\in ℝ\to \left(\neg -A=0\leftrightarrow A\ne 0\right)$$
6	5	biimpa	$$⊢\left(A\in ℝ\wedge \neg -A=0\right)\to A\ne 0$$
7		lt0neg2	$$⊢A\in ℝ\to \left(0<A\leftrightarrow -A<0\right)$$
8	7	adantr	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(0<A\leftrightarrow -A<0\right)$$
9		id	$$⊢A\in ℝ\to A\in ℝ$$
10		0red	$$⊢A\in ℝ\to 0\in ℝ$$
11	9 10	lttri2d	$$⊢A\in ℝ\to \left(A\ne 0\leftrightarrow \left(A<0\vee 0<A\right)\right)$$
12	11	biimpa	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(A<0\vee 0<A\right)$$
13		ltnsym2	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to \neg \left(A<0\wedge 0<A\right)$$
14	10 13	mpdan	$$⊢A\in ℝ\to \neg \left(A<0\wedge 0<A\right)$$
15	14	adantr	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \neg \left(A<0\wedge 0<A\right)$$
16	12 15	jca	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(A<0\vee 0<A\right)\wedge \neg \left(A<0\wedge 0<A\right)\right)$$
17		pm5.17	$$⊢\left(\left(A<0\vee 0<A\right)\wedge \neg \left(A<0\wedge 0<A\right)\right)\leftrightarrow \left(A<0\leftrightarrow \neg 0<A\right)$$
18	16 17	sylib	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(A<0\leftrightarrow \neg 0<A\right)$$
19	18	con2bid	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(0<A\leftrightarrow \neg A<0\right)$$
20	8 19	bitr3d	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(-A<0\leftrightarrow \neg A<0\right)$$
21	20	ifbid	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to if\left(-A<0,-1,1\right)=if\left(\neg A<0,-1,1\right)$$
22		ifnot	$$⊢if\left(\neg A<0,-1,1\right)=if\left(A<0,1,-1\right)$$
23	21 22	eqtrdi	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to if\left(-A<0,-1,1\right)=if\left(A<0,1,-1\right)$$
24	6 23	syldan	$$⊢\left(A\in ℝ\wedge \neg -A=0\right)\to if\left(-A<0,-1,1\right)=if\left(A<0,1,-1\right)$$
25	3 4 24	ifbieq12d2	$$⊢A\in ℝ\to if\left(-A=0,0,if\left(-A<0,-1,1\right)\right)=if\left(A=0,0,if\left(A<0,1,-1\right)\right)$$
26		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
27		rexr	$$⊢-A\in ℝ\to -A\in {ℝ}^{*}$$
28		sgnval	$$⊢-A\in {ℝ}^{*}\to \mathrm{sgn}\left(-A\right)=if\left(-A=0,0,if\left(-A<0,-1,1\right)\right)$$
29	26 27 28	3syl	$$⊢A\in ℝ\to \mathrm{sgn}\left(-A\right)=if\left(-A=0,0,if\left(-A<0,-1,1\right)\right)$$
30		df-neg	$$⊢-\mathrm{sgn}\left(A\right)=0-\mathrm{sgn}\left(A\right)$$
31	30	a1i	$$⊢A\in ℝ\to -\mathrm{sgn}\left(A\right)=0-\mathrm{sgn}\left(A\right)$$
32		rexr	$$⊢A\in ℝ\to A\in {ℝ}^{*}$$
33		sgnval	$$⊢A\in {ℝ}^{*}\to \mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
34	32 33	syl	$$⊢A\in ℝ\to \mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
35	34	oveq2d	$$⊢A\in ℝ\to 0-\mathrm{sgn}\left(A\right)=0-if\left(A=0,0,if\left(A<0,-1,1\right)\right)$$
36		ovif2	$$⊢0-if\left(A=0,0,if\left(A<0,-1,1\right)\right)=if\left(A=0,0-0,0-if\left(A<0,-1,1\right)\right)$$
37		biid	$$⊢A=0\leftrightarrow A=0$$
38		0m0e0	$$⊢0-0=0$$
39		ovif2	$$⊢0-if\left(A<0,-1,1\right)=if\left(A<0,0--1,0-1\right)$$
40		biid	$$⊢A<0\leftrightarrow A<0$$
41		0cn	$$⊢0\in ℂ$$
42		ax-1cn	$$⊢1\in ℂ$$
43	41 42	subnegi	$$⊢0--1=0+1$$
44		0p1e1	$$⊢0+1=1$$
45	43 44	eqtr2i	$$⊢1=0--1$$
46		df-neg	$$⊢-1=0-1$$
47	40 45 46	ifbieq12i	$$⊢if\left(A<0,1,-1\right)=if\left(A<0,0--1,0-1\right)$$
48	39 47	eqtr4i	$$⊢0-if\left(A<0,-1,1\right)=if\left(A<0,1,-1\right)$$
49	37 38 48	ifbieq12i	$$⊢if\left(A=0,0-0,0-if\left(A<0,-1,1\right)\right)=if\left(A=0,0,if\left(A<0,1,-1\right)\right)$$
50	36 49	eqtri	$$⊢0-if\left(A=0,0,if\left(A<0,-1,1\right)\right)=if\left(A=0,0,if\left(A<0,1,-1\right)\right)$$
51	50	a1i	$$⊢A\in ℝ\to 0-if\left(A=0,0,if\left(A<0,-1,1\right)\right)=if\left(A=0,0,if\left(A<0,1,-1\right)\right)$$
52	31 35 51	3eqtrd	$$⊢A\in ℝ\to -\mathrm{sgn}\left(A\right)=if\left(A=0,0,if\left(A<0,1,-1\right)\right)$$
53	25 29 52	3eqtr4d	$$⊢A\in ℝ\to \mathrm{sgn}\left(-A\right)=-\mathrm{sgn}\left(A\right)$$