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	syl6bi	|- ( ( 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	syl6bi	|- ( ( 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		xaddid1	|- ( 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 ) ) )