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	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow \left(A=0\wedge B=0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$
2		elxnn0	$$⊢B\in {\mathbb{N}}_0^{*}\leftrightarrow \left(B\in {\mathbb{N}}_0\vee B=\mathrm{+\infty }\right)$$
3		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
4		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
5		rexadd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A{+}_{𝑒}B=A+B$$
6	3 4 5	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A{+}_{𝑒}B=A+B$$
7	6	eqeq1d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow A+B=0\right)$$
8		nn0ge0	$$⊢A\in {\mathbb{N}}_0\to 0\le A$$
9	3 8	jca	$$⊢A\in {\mathbb{N}}_0\to \left(A\in ℝ\wedge 0\le A\right)$$
10		nn0ge0	$$⊢B\in {\mathbb{N}}_0\to 0\le B$$
11	4 10	jca	$$⊢B\in {\mathbb{N}}_0\to \left(B\in ℝ\wedge 0\le B\right)$$
12		add20	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(A+B=0\leftrightarrow \left(A=0\wedge B=0\right)\right)$$
13	9 11 12	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A+B=0\leftrightarrow \left(A=0\wedge B=0\right)\right)$$
14	7 13	bitrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow \left(A=0\wedge B=0\right)\right)$$
15	14	biimpd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)$$
16	15	expcom	$$⊢B\in {\mathbb{N}}_0\to \left(A\in {\mathbb{N}}_0\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
17		oveq2	$$⊢B=\mathrm{+\infty }\to A{+}_{𝑒}B=A{+}_{𝑒}\mathrm{+\infty }$$
18	17	eqeq1d	$$⊢B=\mathrm{+\infty }\to \left(A{+}_{𝑒}B=0\leftrightarrow A{+}_{𝑒}\mathrm{+\infty }=0\right)$$
19	18	adantr	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow A{+}_{𝑒}\mathrm{+\infty }=0\right)$$
20		nn0xnn0	$$⊢A\in {\mathbb{N}}_0\to A\in {\mathbb{N}}_0^{*}$$
21		xnn0xrnemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$
22		xaddpnf1	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
23	20 21 22	3syl	$$⊢A\in {\mathbb{N}}_0\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
24	23	adantl	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0\right)\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
25	24	eqeq1d	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}\mathrm{+\infty }=0\leftrightarrow \mathrm{+\infty }=0\right)$$
26	19 25	bitrd	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow \mathrm{+\infty }=0\right)$$
27		0re	$$⊢0\in ℝ$$
28		renepnf	$$⊢0\in ℝ\to 0\ne \mathrm{+\infty }$$
29	27 28	ax-mp	$$⊢0\ne \mathrm{+\infty }$$
30	29	nesymi	$$⊢\neg \mathrm{+\infty }=0$$
31	30	pm2.21i	$$⊢\mathrm{+\infty }=0\to \left(A=0\wedge B=0\right)$$
32	26 31	syl6bi	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)$$
33	32	ex	$$⊢B=\mathrm{+\infty }\to \left(A\in {\mathbb{N}}_0\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
34	16 33	jaoi	$$⊢\left(B\in {\mathbb{N}}_0\vee B=\mathrm{+\infty }\right)\to \left(A\in {\mathbb{N}}_0\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
35	2 34	sylbi	$$⊢B\in {\mathbb{N}}_0^{*}\to \left(A\in {\mathbb{N}}_0\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
36	35	com12	$$⊢A\in {\mathbb{N}}_0\to \left(B\in {\mathbb{N}}_0^{*}\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
37		oveq1	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}B=\mathrm{+\infty }{+}_{𝑒}B$$
38	37	eqeq1d	$$⊢A=\mathrm{+\infty }\to \left(A{+}_{𝑒}B=0\leftrightarrow \mathrm{+\infty }{+}_{𝑒}B=0\right)$$
39		xnn0xrnemnf	$$⊢B\in {\mathbb{N}}_0^{*}\to \left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)$$
40		xaddpnf2	$$⊢\left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}B=\mathrm{+\infty }$$
41	39 40	syl	$$⊢B\in {\mathbb{N}}_0^{*}\to \mathrm{+\infty }{+}_{𝑒}B=\mathrm{+\infty }$$
42	41	eqeq1d	$$⊢B\in {\mathbb{N}}_0^{*}\to \left(\mathrm{+\infty }{+}_{𝑒}B=0\leftrightarrow \mathrm{+\infty }=0\right)$$
43	38 42	sylan9bb	$$⊢\left(A=\mathrm{+\infty }\wedge B\in {\mathbb{N}}_0^{*}\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow \mathrm{+\infty }=0\right)$$
44	43 31	syl6bi	$$⊢\left(A=\mathrm{+\infty }\wedge B\in {\mathbb{N}}_0^{*}\right)\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)$$
45	44	ex	$$⊢A=\mathrm{+\infty }\to \left(B\in {\mathbb{N}}_0^{*}\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
46	36 45	jaoi	$$⊢\left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)\to \left(B\in {\mathbb{N}}_0^{*}\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
47	1 46	sylbi	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(B\in {\mathbb{N}}_0^{*}\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)\right)$$
48	47	imp	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to \left(A{+}_{𝑒}B=0\to \left(A=0\wedge B=0\right)\right)$$
49		oveq12	$$⊢\left(A=0\wedge B=0\right)\to A{+}_{𝑒}B=0{+}_{𝑒}0$$
50		0xr	$$⊢0\in {ℝ}^{*}$$
51		xaddid1	$$⊢0\in {ℝ}^{*}\to 0{+}_{𝑒}0=0$$
52	50 51	ax-mp	$$⊢0{+}_{𝑒}0=0$$
53	49 52	eqtrdi	$$⊢\left(A=0\wedge B=0\right)\to A{+}_{𝑒}B=0$$
54	48 53	impbid1	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to \left(A{+}_{𝑒}B=0\leftrightarrow \left(A=0\wedge B=0\right)\right)$$