Theorem xnegneg

Description: Extended real version of negneg . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegneg	$$⊢A\in {ℝ}^{*}\to -\left(-A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢A\in {ℝ}^{*}\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)$$
2		rexneg	$$⊢A\in ℝ\to -A=-A$$
3		xnegeq	$$⊢-A=-A\to -\left(-A\right)=-\left(-A\right)$$
4	2 3	syl	$$⊢A\in ℝ\to -\left(-A\right)=-\left(-A\right)$$
5		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
6		rexneg	$$⊢-A\in ℝ\to -\left(-A\right)=-\left(-A\right)$$
7	5 6	syl	$$⊢A\in ℝ\to -\left(-A\right)=-\left(-A\right)$$
8		recn	$$⊢A\in ℝ\to A\in ℂ$$
9	8	negnegd	$$⊢A\in ℝ\to -\left(-A\right)=A$$
10	4 7 9	3eqtrd	$$⊢A\in ℝ\to -\left(-A\right)=A$$
11		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
12		xnegeq	$$⊢A=\mathrm{+\infty }\to -A=-\mathrm{+\infty }$$
13		xnegpnf	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$
14	12 13	eqtrdi	$$⊢A=\mathrm{+\infty }\to -A=\mathrm{-\infty }$$
15		xnegeq	$$⊢-A=\mathrm{-\infty }\to -\left(-A\right)=-\mathrm{-\infty }$$
16	14 15	syl	$$⊢A=\mathrm{+\infty }\to -\left(-A\right)=-\mathrm{-\infty }$$
17		id	$$⊢A=\mathrm{+\infty }\to A=\mathrm{+\infty }$$
18	11 16 17	3eqtr4a	$$⊢A=\mathrm{+\infty }\to -\left(-A\right)=A$$
19		xnegeq	$$⊢A=\mathrm{-\infty }\to -A=-\mathrm{-\infty }$$
20	19 11	eqtrdi	$$⊢A=\mathrm{-\infty }\to -A=\mathrm{+\infty }$$
21		xnegeq	$$⊢-A=\mathrm{+\infty }\to -\left(-A\right)=-\mathrm{+\infty }$$
22	20 21	syl	$$⊢A=\mathrm{-\infty }\to -\left(-A\right)=-\mathrm{+\infty }$$
23		id	$$⊢A=\mathrm{-\infty }\to A=\mathrm{-\infty }$$
24	13 22 23	3eqtr4a	$$⊢A=\mathrm{-\infty }\to -\left(-A\right)=A$$
25	10 18 24	3jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)\to -\left(-A\right)=A$$
26	1 25	sylbi	$$⊢A\in {ℝ}^{*}\to -\left(-A\right)=A$$