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

Metamath Proof Explorer

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 )