Theorem n0mulscl

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=0_s\to A{\cdot }_{s}n=A{\cdot }_s{0}_s$$
2	1	eleq1d	$$⊢n=0_s\to \left(A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{\cdot }_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{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
4		oveq2	$$⊢n=m\to A{\cdot }_{s}n=A{\cdot }_{s}m$$
5	4	eleq1d	$$⊢n=m\to \left(A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
6	5	imbi2d	$$⊢n=m\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
7		oveq2	$$⊢n=m{+}_s{1}_s\to A{\cdot }_{s}n=A{\cdot }_s\left(m{+}_s{1}_s\right)$$
8	7	eleq1d	$$⊢n=m{+}_s{1}_s\to \left(A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{\cdot }_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{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
10		oveq2	$$⊢n=B\to A{\cdot }_{s}n=A{\cdot }_{s}B$$
11	10	eleq1d	$$⊢n=B\to \left(A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow A{\cdot }_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
12	11	imbi2d	$$⊢n=B\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}n\in {\mathbb{N}}_{\mathrm{0s}}\right)\leftrightarrow \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
13		n0sno	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
14		muls01	$$⊢A\in \mathrm{No}\to A{\cdot }_s{0}_s=0_s$$
15	13 14	syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s{0}_s=0_s$$
16		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
17	15 16	eqeltrdi	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s{0}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
18	13	ad2antrr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{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	ad2antlr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to m\in \mathrm{No}$$
21		1sno	$$⊢1_s\in \mathrm{No}$$
22	21	a1i	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to 1_s\in \mathrm{No}$$
23	18 20 22	addsdid	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{\cdot }_s\left(m{+}_s{1}_s\right)=\left(A{\cdot }_{s}m\right){+}_s\left(A{\cdot }_s{1}_s\right)$$
24	13	mulsridd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s{1}_s=A$$
25	24	oveq2d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{\cdot }_{s}m\right){+}_s\left(A{\cdot }_s{1}_s\right)=\left(A{\cdot }_{s}m\right){+}_{s}A$$
26	25	ad2antrr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\cdot }_{s}m\right){+}_s\left(A{\cdot }_s{1}_s\right)=\left(A{\cdot }_{s}m\right){+}_{s}A$$
27	23 26	eqtrd	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{\cdot }_s\left(m{+}_s{1}_s\right)=\left(A{\cdot }_{s}m\right){+}_{s}A$$
28		n0addscl	$$⊢\left(A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\wedge A\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\cdot }_{s}m\right){+}_{s}A\in {\mathbb{N}}_{\mathrm{0s}}$$
29	28	ancoms	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\cdot }_{s}m\right){+}_{s}A\in {\mathbb{N}}_{\mathrm{0s}}$$
30	29	adantlr	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\cdot }_{s}m\right){+}_{s}A\in {\mathbb{N}}_{\mathrm{0s}}$$
31	27 30	eqeltrd	$$⊢\left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\wedge A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{\cdot }_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}$$
32	31	ex	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
33	32	expcom	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
34	33	a2d	$$⊢m\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}m\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_s\left(m{+}_s{1}_s\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
35	3 6 9 12 17 34	n0sind	$$⊢B\in {\mathbb{N}}_{\mathrm{0s}}\to \left(A\in {\mathbb{N}}_{\mathrm{0s}}\to A{\cdot }_{s}B\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
36	35	impcom	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge B\in {\mathbb{N}}_{\mathrm{0s}}\right)\to A{\cdot }_{s}B\in {\mathbb{N}}_{\mathrm{0s}}$$