This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )