Metamath Proof Explorer

Theorem xnn0xaddcl

Description: The extended nonnegative integers are closed under extended addition. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0xaddcl 
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* )

Proof

Step Hyp Ref Expression
1 nn0addcl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) e. NN0 )
2 1 nn0xnn0d 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) e. NN0* )
3 nn0re 
 |-  ( A e. NN0 -> A e. RR )
4 nn0re 
 |-  ( B e. NN0 -> B e. RR )
5 rexadd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
6 5 eleq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A +e B ) e. NN0* <-> ( A + B ) e. NN0* ) )
7 3 4 6 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A +e B ) e. NN0* <-> ( A + B ) e. NN0* ) )
8 2 7 mpbird 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A +e B ) e. NN0* )
9 8 a1d 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* ) )
10 ianor 
 |-  ( -. ( A e. NN0 /\ B e. NN0 ) <-> ( -. A e. NN0 \/ -. B e. NN0 ) )
11 xnn0nnn0pnf 
 |-  ( ( A e. NN0* /\ -. A e. NN0 ) -> A = +oo )
12 oveq1 
 |-  ( A = +oo -> ( A +e B ) = ( +oo +e B ) )
13 xnn0xrnemnf 
 |-  ( B e. NN0* -> ( B e. RR* /\ B =/= -oo ) )
14 xaddpnf2 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )
15 13 14 syl 
 |-  ( B e. NN0* -> ( +oo +e B ) = +oo )
16 12 15 sylan9eq 
 |-  ( ( A = +oo /\ B e. NN0* ) -> ( A +e B ) = +oo )
17 16 ex 
 |-  ( A = +oo -> ( B e. NN0* -> ( A +e B ) = +oo ) )
18 11 17 syl 
 |-  ( ( A e. NN0* /\ -. A e. NN0 ) -> ( B e. NN0* -> ( A +e B ) = +oo ) )
19 18 expcom 
 |-  ( -. A e. NN0 -> ( A e. NN0* -> ( B e. NN0* -> ( A +e B ) = +oo ) ) )
20 19 impd 
 |-  ( -. A e. NN0 -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) = +oo ) )
21 xnn0nnn0pnf 
 |-  ( ( B e. NN0* /\ -. B e. NN0 ) -> B = +oo )
22 oveq2 
 |-  ( B = +oo -> ( A +e B ) = ( A +e +oo ) )
23 xnn0xrnemnf 
 |-  ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )
24 xaddpnf1 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
25 23 24 syl 
 |-  ( A e. NN0* -> ( A +e +oo ) = +oo )
26 22 25 sylan9eq 
 |-  ( ( B = +oo /\ A e. NN0* ) -> ( A +e B ) = +oo )
27 26 ex 
 |-  ( B = +oo -> ( A e. NN0* -> ( A +e B ) = +oo ) )
28 21 27 syl 
 |-  ( ( B e. NN0* /\ -. B e. NN0 ) -> ( A e. NN0* -> ( A +e B ) = +oo ) )
29 28 expcom 
 |-  ( -. B e. NN0 -> ( B e. NN0* -> ( A e. NN0* -> ( A +e B ) = +oo ) ) )
30 29 impcomd 
 |-  ( -. B e. NN0 -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) = +oo ) )
31 20 30 jaoi 
 |-  ( ( -. A e. NN0 \/ -. B e. NN0 ) -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) = +oo ) )
32 31 imp 
 |-  ( ( ( -. A e. NN0 \/ -. B e. NN0 ) /\ ( A e. NN0* /\ B e. NN0* ) ) -> ( A +e B ) = +oo )
33 pnf0xnn0 
 |-  +oo e. NN0*
34 32 33 eqeltrdi 
 |-  ( ( ( -. A e. NN0 \/ -. B e. NN0 ) /\ ( A e. NN0* /\ B e. NN0* ) ) -> ( A +e B ) e. NN0* )
35 34 ex 
 |-  ( ( -. A e. NN0 \/ -. B e. NN0 ) -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* ) )
36 10 35 sylbi 
 |-  ( -. ( A e. NN0 /\ B e. NN0 ) -> ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* ) )
37 9 36 pm2.61i 
 |-  ( ( A e. NN0* /\ B e. NN0* ) -> ( A +e B ) e. NN0* )