Theorem xaddnepnf

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

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

Proof

Step	Hyp	Ref	Expression
1		xrnepnf	|- ( ( A e. RR* /\ A =/= +oo ) <-> ( A e. RR \/ A = -oo ) )
2		xrnepnf	|- ( ( 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	renepnfd	|- ( ( 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		renepnf	|- ( A e. RR -> A =/= +oo )
10		xaddmnf1	|- ( ( 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		mnfnepnf	|- -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		xaddmnf2	|- ( ( 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 )