Theorem xaddnemnf

Description: Closure of extended real addition in the subset RR* / { -oo } . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xaddnemnf	|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )

Proof

Step	Hyp	Ref	Expression
1		xrnemnf	|- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
2		xrnemnf	|- ( ( B e. RR* /\ B =/= -oo ) <-> ( B e. RR \/ B = +oo ) )
3		rexadd	|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
4		readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
5	3 4	eqeltrd	|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) e. RR )
6	5	renemnfd	|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) =/= -oo )
7		oveq2	|- ( B = +oo -> ( A +e B ) = ( A +e +oo ) )
8		rexr	|- ( A e. RR -> A e. RR* )
9		renemnf	|- ( A e. RR -> A =/= -oo )
10		xaddpnf1	|- ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
11	8 9 10	syl2anc	|- ( A e. RR -> ( A +e +oo ) = +oo )
12	7 11	sylan9eqr	|- ( ( A e. RR /\ B = +oo ) -> ( A +e B ) = +oo )
13		pnfnemnf	|- +oo =/= -oo
14	13	a1i	|- ( ( A e. RR /\ B = +oo ) -> +oo =/= -oo )
15	12 14	eqnetrd	|- ( ( A e. RR /\ B = +oo ) -> ( A +e B ) =/= -oo )
16	6 15	jaodan	|- ( ( A e. RR /\ ( B e. RR \/ B = +oo ) ) -> ( A +e B ) =/= -oo )
17	2 16	sylan2b	|- ( ( A e. RR /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
18		oveq1	|- ( A = +oo -> ( A +e B ) = ( +oo +e B ) )
19		xaddpnf2	|- ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )
20	18 19	sylan9eq	|- ( ( A = +oo /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) = +oo )
21	13	a1i	|- ( ( A = +oo /\ ( B e. RR* /\ B =/= -oo ) ) -> +oo =/= -oo )
22	20 21	eqnetrd	|- ( ( A = +oo /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
23	17 22	jaoian	|- ( ( ( A e. RR \/ A = +oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
24	1 23	sylanb	|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )