Theorem xnegid

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

	Ref	Expression
Assertion	xnegid	|- ( A e. RR* -> ( A +e -e A ) = 0 )

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	2	oveq2d	|- ( A e. RR -> ( A +e -e A ) = ( A +e -u A ) )
4		renegcl	|- ( A e. RR -> -u A e. RR )
5		rexadd	|- ( ( A e. RR /\ -u A e. RR ) -> ( A +e -u A ) = ( A + -u A ) )
6	4 5	mpdan	|- ( A e. RR -> ( A +e -u A ) = ( A + -u A ) )
7		recn	|- ( A e. RR -> A e. CC )
8	7	negidd	|- ( A e. RR -> ( A + -u A ) = 0 )
9	3 6 8	3eqtrd	|- ( A e. RR -> ( A +e -e A ) = 0 )
10		id	|- ( A = +oo -> A = +oo )
11		xnegeq	|- ( A = +oo -> -e A = -e +oo )
12		xnegpnf	|- -e +oo = -oo
13	11 12	eqtrdi	|- ( A = +oo -> -e A = -oo )
14	10 13	oveq12d	|- ( A = +oo -> ( A +e -e A ) = ( +oo +e -oo ) )
15		pnfaddmnf	|- ( +oo +e -oo ) = 0
16	14 15	eqtrdi	|- ( A = +oo -> ( A +e -e A ) = 0 )
17		id	|- ( A = -oo -> A = -oo )
18		xnegeq	|- ( A = -oo -> -e A = -e -oo )
19		xnegmnf	|- -e -oo = +oo
20	18 19	eqtrdi	|- ( A = -oo -> -e A = +oo )
21	17 20	oveq12d	|- ( A = -oo -> ( A +e -e A ) = ( -oo +e +oo ) )
22		mnfaddpnf	|- ( -oo +e +oo ) = 0
23	21 22	eqtrdi	|- ( A = -oo -> ( A +e -e A ) = 0 )
24	9 16 23	3jaoi	|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A +e -e A ) = 0 )
25	1 24	sylbi	|- ( A e. RR* -> ( A +e -e A ) = 0 )