Theorem n0addscl

Description: The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	n0addscl	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{+}_{s}B\in {\mathbb{N}}_{\mathrm{0s}}$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=0_s\to A{+}_{s}n=A{+}_s{0}_s$$
2	1	eleq1d	$$⊢n=0_s\to \left(A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{+}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
3	2	imbi2d	$$⊢n=0_s\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
4		oveq2	$$⊢n=m\to A{+}_{s}n=A{+}_{s}m$$
5	4	eleq1d	$$⊢n=m\to \left(A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
6	5	imbi2d	$$⊢n=m\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
7		oveq2	$$⊢n=m{+}_s{1}_s\to A{+}_{s}n=A{+}_s\left(m{+}_s{1}_s\right)$$
8	7	eleq1d	$$⊢n=m{+}_s{1}_s\to \left(A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
9	8	imbi2d	$$⊢n=m{+}_s{1}_s\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
10		oveq2	$$⊢n=B\to A{+}_{s}n=A{+}_{s}B$$
11	10	eleq1d	$$⊢n=B\to \left(A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{+}_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
12	11	imbi2d	$$⊢n=B\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
13		n0sno	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
14	13	addsridd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{0}_s=A$$
15		id	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {\mathbb{N}}_{\mathrm{0s}}$$
16	14 15	eqeltrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
17	13	adantr	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
18	17	adantr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A\in \mathrm{No}$$
19		n0sno	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to m\in \mathrm{No}$$
20	19	adantl	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to m\in \mathrm{No}$$
21	20	adantr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to m\in \mathrm{No}$$
22		1sno	$$⊢1_s\in \mathrm{No}$$
23	22	a1i	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in \mathrm{No}$$
24	18 21 23	addsassd	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{+}_{s}m\right){+}_s{1}_s=A{+}_s\left(m{+}_s{1}_s\right)$$
25		peano2n0s	$$⊢A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{+}_{s}m\right){+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
26	25	adantl	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{+}_{s}m\right){+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
27	24 26	eqeltrrd	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
28	27	ex	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
29	28	expcom	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
30	29	a2d	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
31	3 6 9 12 16 30	n0sind	$$⊢B\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{+}_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
32	31	impcom	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{+}_{s}B\in {\mathbb{N}}_{\mathrm{0s}}$$