Theorem xaddid1

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

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

Proof

Step	Hyp	Ref	Expression
1		elxr	|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2		0re	|- 0 e. RR
3		rexadd	|- ( ( A e. RR /\ 0 e. RR ) -> ( A +e 0 ) = ( A + 0 ) )
4	2 3	mpan2	|- ( A e. RR -> ( A +e 0 ) = ( A + 0 ) )
5		recn	|- ( A e. RR -> A e. CC )
6	5	addid1d	|- ( A e. RR -> ( A + 0 ) = A )
7	4 6	eqtrd	|- ( A e. RR -> ( A +e 0 ) = A )
8		0xr	|- 0 e. RR*
9		renemnf	|- ( 0 e. RR -> 0 =/= -oo )
10	2 9	ax-mp	|- 0 =/= -oo
11		xaddpnf2	|- ( ( 0 e. RR* /\ 0 =/= -oo ) -> ( +oo +e 0 ) = +oo )
12	8 10 11	mp2an	|- ( +oo +e 0 ) = +oo
13		oveq1	|- ( A = +oo -> ( A +e 0 ) = ( +oo +e 0 ) )
14		id	|- ( A = +oo -> A = +oo )
15	12 13 14	3eqtr4a	|- ( A = +oo -> ( A +e 0 ) = A )
16		renepnf	|- ( 0 e. RR -> 0 =/= +oo )
17	2 16	ax-mp	|- 0 =/= +oo
18		xaddmnf2	|- ( ( 0 e. RR* /\ 0 =/= +oo ) -> ( -oo +e 0 ) = -oo )
19	8 17 18	mp2an	|- ( -oo +e 0 ) = -oo
20		oveq1	|- ( A = -oo -> ( A +e 0 ) = ( -oo +e 0 ) )
21		id	|- ( A = -oo -> A = -oo )
22	19 20 21	3eqtr4a	|- ( A = -oo -> ( A +e 0 ) = A )
23	7 15 22	3jaoi	|- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A +e 0 ) = A )
24	1 23	sylbi	|- ( A e. RR* -> ( A +e 0 ) = A )