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

Metamath Proof Explorer

Theorem xnn0xadd0

Description: The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0 . (Contributed by AV, 14-Dec-2020)

Ref Expression
Assertion xnn0xadd0 
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )

Proof

Step Hyp Ref Expression
1 elxnn0 
 |-  ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) )
2 elxnn0 
 |-  ( B e. NN0* <-> ( B e. NN0 \/ B = +oo ) )
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 3 4 5 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A +e B ) = ( A + B ) )
7 6 eqeq1d 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A +e B ) = 0 <-> ( A + B ) = 0 ) )
8 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
9 3 8 jca 
 |-  ( A e. NN0 -> ( A e. RR /\ 0 <_ A ) )
10 nn0ge0 
 |-  ( B e. NN0 -> 0 <_ B )
11 4 10 jca 
 |-  ( B e. NN0 -> ( B e. RR /\ 0 <_ B ) )
12 add20 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
13 9 11 12 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
14 7 13 bitrd 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
15 14 biimpd 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) )
16 15 expcom 
 |-  ( B e. NN0 -> ( A e. NN0 -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
17 oveq2 
 |-  ( B = +oo -> ( A +e B ) = ( A +e +oo ) )
18 17 eqeq1d 
 |-  ( B = +oo -> ( ( A +e B ) = 0 <-> ( A +e +oo ) = 0 ) )
19 18 adantr 
 |-  ( ( B = +oo /\ A e. NN0 ) -> ( ( A +e B ) = 0 <-> ( A +e +oo ) = 0 ) )
20 nn0xnn0 
 |-  ( A e. NN0 -> A e. NN0* )
21 xnn0xrnemnf 
 |-  ( A e. NN0* -> ( A e. RR* /\ A =/= -oo ) )
22 xaddpnf1 
 |-  ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
23 20 21 22 3syl 
 |-  ( A e. NN0 -> ( A +e +oo ) = +oo )
24 23 adantl 
 |-  ( ( B = +oo /\ A e. NN0 ) -> ( A +e +oo ) = +oo )
25 24 eqeq1d 
 |-  ( ( B = +oo /\ A e. NN0 ) -> ( ( A +e +oo ) = 0 <-> +oo = 0 ) )
26 19 25 bitrd 
 |-  ( ( B = +oo /\ A e. NN0 ) -> ( ( A +e B ) = 0 <-> +oo = 0 ) )
27 0re 
 |-  0 e. RR
28 renepnf 
 |-  ( 0 e. RR -> 0 =/= +oo )
29 27 28 ax-mp 
 |-  0 =/= +oo
30 29 nesymi 
 |-  -. +oo = 0
31 30 pm2.21i 
 |-  ( +oo = 0 -> ( A = 0 /\ B = 0 ) )
32 26 31 biimtrdi 
 |-  ( ( B = +oo /\ A e. NN0 ) -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) )
33 32 ex 
 |-  ( B = +oo -> ( A e. NN0 -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
34 16 33 jaoi 
 |-  ( ( B e. NN0 \/ B = +oo ) -> ( A e. NN0 -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
35 2 34 sylbi 
 |-  ( B e. NN0* -> ( A e. NN0 -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
36 35 com12 
 |-  ( A e. NN0 -> ( B e. NN0* -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
37 oveq1 
 |-  ( A = +oo -> ( A +e B ) = ( +oo +e B ) )
38 37 eqeq1d 
 |-  ( A = +oo -> ( ( A +e B ) = 0 <-> ( +oo +e B ) = 0 ) )
39 xnn0xrnemnf 
 |-  ( B e. NN0* -> ( B e. RR* /\ B =/= -oo ) )
40 xaddpnf2 
 |-  ( ( B e. RR* /\ B =/= -oo ) -> ( +oo +e B ) = +oo )
41 39 40 syl 
 |-  ( B e. NN0* -> ( +oo +e B ) = +oo )
42 41 eqeq1d 
 |-  ( B e. NN0* -> ( ( +oo +e B ) = 0 <-> +oo = 0 ) )
43 38 42 sylan9bb 
 |-  ( ( A = +oo /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> +oo = 0 ) )
44 43 31 biimtrdi 
 |-  ( ( A = +oo /\ B e. NN0* ) -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) )
45 44 ex 
 |-  ( A = +oo -> ( B e. NN0* -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
46 36 45 jaoi 
 |-  ( ( A e. NN0 \/ A = +oo ) -> ( B e. NN0* -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
47 1 46 sylbi 
 |-  ( A e. NN0* -> ( B e. NN0* -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) ) )
48 47 imp 
 |-  ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 -> ( A = 0 /\ B = 0 ) ) )
49 oveq12 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A +e B ) = ( 0 +e 0 ) )
50 0xr 
 |-  0 e. RR*
51 xaddrid 
 |-  ( 0 e. RR* -> ( 0 +e 0 ) = 0 )
52 50 51 ax-mp 
 |-  ( 0 +e 0 ) = 0
53 49 52 eqtrdi 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A +e B ) = 0 )
54 48 53 impbid1 
 |-  ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )