Theorem xnn0xaddcl

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

	Ref	Expression
Assertion	xnn0xaddcl	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		nn0addcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A+B\in {\mathbb{N}}_0$$
2	1	nn0xnn0d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A+B\in {\mathbb{N}}_0^{*}$$
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	5	eleq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}\leftrightarrow A+B\in {\mathbb{N}}_0^{*}\right)$$
7	3 4 6	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}\leftrightarrow A+B\in {\mathbb{N}}_0^{*}\right)$$
8	2 7	mpbird	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}$$
9	8	a1d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}\right)$$
10		ianor	$$⊢\neg \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\leftrightarrow \left(\neg A\in {\mathbb{N}}_0\vee \neg B\in {\mathbb{N}}_0\right)$$
11		xnn0nnn0pnf	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge \neg A\in {\mathbb{N}}_0\right)\to A=\mathrm{+\infty }$$
12		oveq1	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}B=\mathrm{+\infty }{+}_{𝑒}B$$
13		xnn0xrnemnf	$$⊢B\in {\mathbb{N}}_0^{*}\to \left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)$$
14		xaddpnf2	$$⊢\left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}B=\mathrm{+\infty }$$
15	13 14	syl	$$⊢B\in {\mathbb{N}}_0^{*}\to \mathrm{+\infty }{+}_{𝑒}B=\mathrm{+\infty }$$
16	12 15	sylan9eq	$$⊢\left(A=\mathrm{+\infty }\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B=\mathrm{+\infty }$$
17	16	ex	$$⊢A=\mathrm{+\infty }\to \left(B\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
18	11 17	syl	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge \neg A\in {\mathbb{N}}_0\right)\to \left(B\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
19	18	expcom	$$⊢\neg A\in {\mathbb{N}}_0\to \left(A\in {\mathbb{N}}_0^{*}\to \left(B\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)\right)$$
20	19	impd	$$⊢\neg A\in {\mathbb{N}}_0\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
21		xnn0nnn0pnf	$$⊢\left(B\in {\mathbb{N}}_0^{*}\wedge \neg B\in {\mathbb{N}}_0\right)\to B=\mathrm{+\infty }$$
22		oveq2	$$⊢B=\mathrm{+\infty }\to A{+}_{𝑒}B=A{+}_{𝑒}\mathrm{+\infty }$$
23		xnn0xrnemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$
24		xaddpnf1	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
25	23 24	syl	$$⊢A\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
26	22 25	sylan9eq	$$⊢\left(B=\mathrm{+\infty }\wedge A\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B=\mathrm{+\infty }$$
27	26	ex	$$⊢B=\mathrm{+\infty }\to \left(A\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
28	21 27	syl	$$⊢\left(B\in {\mathbb{N}}_0^{*}\wedge \neg B\in {\mathbb{N}}_0\right)\to \left(A\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
29	28	expcom	$$⊢\neg B\in {\mathbb{N}}_0\to \left(B\in {\mathbb{N}}_0^{*}\to \left(A\in {\mathbb{N}}_0^{*}\to A{+}_{𝑒}B=\mathrm{+\infty }\right)\right)$$
30	29	impcomd	$$⊢\neg B\in {\mathbb{N}}_0\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
31	20 30	jaoi	$$⊢\left(\neg A\in {\mathbb{N}}_0\vee \neg B\in {\mathbb{N}}_0\right)\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B=\mathrm{+\infty }\right)$$
32	31	imp	$$⊢\left(\left(\neg A\in {\mathbb{N}}_0\vee \neg B\in {\mathbb{N}}_0\right)\wedge \left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\right)\to A{+}_{𝑒}B=\mathrm{+\infty }$$
33		pnf0xnn0	$$⊢\mathrm{+\infty }\in {\mathbb{N}}_0^{*}$$
34	32 33	eqeltrdi	$$⊢\left(\left(\neg A\in {\mathbb{N}}_0\vee \neg B\in {\mathbb{N}}_0\right)\wedge \left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}$$
35	34	ex	$$⊢\left(\neg A\in {\mathbb{N}}_0\vee \neg B\in {\mathbb{N}}_0\right)\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}\right)$$
36	10 35	sylbi	$$⊢\neg \left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}\right)$$
37	9 36	pm2.61i	$$⊢\left(A\in {\mathbb{N}}_0^{*}\wedge B\in {\mathbb{N}}_0^{*}\right)\to A{+}_{𝑒}B\in {\mathbb{N}}_0^{*}$$