Theorem xnegneg

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

	Ref	Expression
Assertion	xnegneg	|- ( A e. RR* -> -e -e A = A )

Proof

Step	Hyp	Ref	Expression
1		elxr	|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2		rexneg	|- ( A e. RR -> -e A = -u A )
3		xnegeq	|- ( -e A = -u A -> -e -e A = -e -u A )
4	2 3	syl	|- ( A e. RR -> -e -e A = -e -u A )
5		renegcl	|- ( A e. RR -> -u A e. RR )
6		rexneg	|- ( -u A e. RR -> -e -u A = -u -u A )
7	5 6	syl	|- ( A e. RR -> -e -u A = -u -u A )
8		recn	|- ( A e. RR -> A e. CC )
9	8	negnegd	|- ( A e. RR -> -u -u A = A )
10	4 7 9	3eqtrd	|- ( A e. RR -> -e -e A = A )
11		xnegmnf	|- -e -oo = +oo
12		xnegeq	|- ( A = +oo -> -e A = -e +oo )
13		xnegpnf	|- -e +oo = -oo
14	12 13	syl6eq	|- ( A = +oo -> -e A = -oo )
15		xnegeq	|- ( -e A = -oo -> -e -e A = -e -oo )
16	14 15	syl	|- ( A = +oo -> -e -e A = -e -oo )
17		id	|- ( A = +oo -> A = +oo )
18	11 16 17	3eqtr4a	|- ( A = +oo -> -e -e A = A )
19		xnegeq	|- ( A = -oo -> -e A = -e -oo )
20	19 11	syl6eq	|- ( A = -oo -> -e A = +oo )
21		xnegeq	|- ( -e A = +oo -> -e -e A = -e +oo )
22	20 21	syl	|- ( A = -oo -> -e -e A = -e +oo )
23		id	|- ( A = -oo -> A = -oo )
24	13 22 23	3eqtr4a	|- ( A = -oo -> -e -e A = A )
25	10 18 24	3jaoi	|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> -e -e A = A )
26	1 25	sylbi	|- ( A e. RR* -> -e -e A = A )