Theorem zmulscld

Description: The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025)

	Ref	Expression
Hypotheses	zmulscld.1	$$⊢\phi \to A\in {\mathbb{Z}}_s$$
	zmulscld.2	$$⊢\phi \to B\in {\mathbb{Z}}_s$$
Assertion	zmulscld	$$⊢\phi \to A{\cdot }_{s}B\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		zmulscld.1	$$⊢\phi \to A\in {\mathbb{Z}}_s$$
2		zmulscld.2	$$⊢\phi \to B\in {\mathbb{Z}}_s$$
3		elzs	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
4	1 3	sylib	$$⊢\phi \to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
5		elzs	$$⊢B\in {\mathbb{Z}}_s\leftrightarrow \exists z\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w$$
6	2 5	sylib	$$⊢\phi \to \exists z\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w$$
7		reeanv	$$⊢\exists y\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_s\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\leftrightarrow \left(\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)$$
8	7	2rexbii	$$⊢\exists x\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_s\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\leftrightarrow \exists x\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_s\left(\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)$$
9		reeanv	$$⊢\exists x\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_s\left(\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)\leftrightarrow \left(\exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists z\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)$$
10	8 9	bitri	$$⊢\exists x\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_s\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\leftrightarrow \left(\exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists z\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)$$
11		nnsno	$$⊢x\in {\mathbb{N}}_s\to x\in \mathrm{No}$$
12	11	ad2antrr	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x\in \mathrm{No}$$
13		nnsno	$$⊢y\in {\mathbb{N}}_s\to y\in \mathrm{No}$$
14	13	ad2antrl	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y\in \mathrm{No}$$
15	12 14	subscld	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x{-}_{s}y\in \mathrm{No}$$
16		nnsno	$$⊢z\in {\mathbb{N}}_s\to z\in \mathrm{No}$$
17	16	ad2antlr	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to z\in \mathrm{No}$$
18		nnsno	$$⊢w\in {\mathbb{N}}_s\to w\in \mathrm{No}$$
19	18	ad2antll	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to w\in \mathrm{No}$$
20	15 17 19	subsdid	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{-}_{s}y\right){\cdot }_s\left(z{-}_{s}w\right)=\left(\left(x{-}_{s}y\right){\cdot }_{s}z\right){-}_s\left(\left(x{-}_{s}y\right){\cdot }_{s}w\right)$$
21		nnmulscl	$$⊢\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\to x{\cdot }_{s}z\in {\mathbb{N}}_s$$
22	21	adantr	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x{\cdot }_{s}z\in {\mathbb{N}}_s$$
23	22	nnsnod	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x{\cdot }_{s}z\in \mathrm{No}$$
24		simprl	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y\in {\mathbb{N}}_s$$
25		simplr	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to z\in {\mathbb{N}}_s$$
26		nnmulscl	$$⊢\left(y\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\to y{\cdot }_{s}z\in {\mathbb{N}}_s$$
27	24 25 26	syl2anc	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y{\cdot }_{s}z\in {\mathbb{N}}_s$$
28	27	nnsnod	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y{\cdot }_{s}z\in \mathrm{No}$$
29	23 28	subscld	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)\in \mathrm{No}$$
30		nnmulscl	$$⊢\left(x\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\to x{\cdot }_{s}w\in {\mathbb{N}}_s$$
31	30	ad2ant2rl	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x{\cdot }_{s}w\in {\mathbb{N}}_s$$
32	31	nnsnod	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to x{\cdot }_{s}w\in \mathrm{No}$$
33		nnmulscl	$$⊢\left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\to y{\cdot }_{s}w\in {\mathbb{N}}_s$$
34	33	adantl	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y{\cdot }_{s}w\in {\mathbb{N}}_s$$
35	34	nnsnod	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to y{\cdot }_{s}w\in \mathrm{No}$$
36	29 32 35	subsubs2d	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}w\right){-}_s\left(y{\cdot }_{s}w\right)\right)=\left(\left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(y{\cdot }_{s}w\right){-}_s\left(x{\cdot }_{s}w\right)\right)$$
37	12 14 17	subsdird	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{-}_{s}y\right){\cdot }_{s}z=\left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)$$
38	12 14 19	subsdird	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{-}_{s}y\right){\cdot }_{s}w=\left(x{\cdot }_{s}w\right){-}_s\left(y{\cdot }_{s}w\right)$$
39	37 38	oveq12d	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(x{-}_{s}y\right){\cdot }_{s}z\right){-}_s\left(\left(x{-}_{s}y\right){\cdot }_{s}w\right)=\left(\left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)\right){-}_s\left(\left(x{\cdot }_{s}w\right){-}_s\left(y{\cdot }_{s}w\right)\right)$$
40	23 35 28 32	addsubs4d	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=\left(\left(x{\cdot }_{s}z\right){-}_s\left(y{\cdot }_{s}z\right)\right){+}_s\left(\left(y{\cdot }_{s}w\right){-}_s\left(x{\cdot }_{s}w\right)\right)$$
41	36 39 40	3eqtr4d	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(x{-}_{s}y\right){\cdot }_{s}z\right){-}_s\left(\left(x{-}_{s}y\right){\cdot }_{s}w\right)=\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)$$
42	20 41	eqtrd	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{-}_{s}y\right){\cdot }_s\left(z{-}_{s}w\right)=\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)$$
43		nnaddscl	$$⊢\left(x{\cdot }_{s}z\in {\mathbb{N}}_s\wedge y{\cdot }_{s}w\in {\mathbb{N}}_s\right)\to \left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\in {\mathbb{N}}_s$$
44	22 34 43	syl2anc	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\in {\mathbb{N}}_s$$
45		nnaddscl	$$⊢\left(y{\cdot }_{s}z\in {\mathbb{N}}_s\wedge x{\cdot }_{s}w\in {\mathbb{N}}_s\right)\to \left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\in {\mathbb{N}}_s$$
46	27 31 45	syl2anc	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\in {\mathbb{N}}_s$$
47		eqid	$$⊢\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)$$
48		rspceov	$$⊢\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\in {\mathbb{N}}_s\wedge \left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\in {\mathbb{N}}_s\wedge \left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)\right)\to \exists t\in {\mathbb{N}}_s\exists u\in {\mathbb{N}}_s\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=t{-}_{s}u$$
49	47 48	mp3an3	$$⊢\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\in {\mathbb{N}}_s\wedge \left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\in {\mathbb{N}}_s\right)\to \exists t\in {\mathbb{N}}_s\exists u\in {\mathbb{N}}_s\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=t{-}_{s}u$$
50	44 46 49	syl2anc	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \exists t\in {\mathbb{N}}_s\exists u\in {\mathbb{N}}_s\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=t{-}_{s}u$$
51		elzs	$$⊢\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)\in {\mathbb{Z}}_s\leftrightarrow \exists t\in {\mathbb{N}}_s\exists u\in {\mathbb{N}}_s\left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)=t{-}_{s}u$$
52	50 51	sylibr	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(x{\cdot }_{s}z\right){+}_s\left(y{\cdot }_{s}w\right)\right){-}_s\left(\left(y{\cdot }_{s}z\right){+}_s\left(x{\cdot }_{s}w\right)\right)\in {\mathbb{Z}}_s$$
53	42 52	eqeltrd	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(x{-}_{s}y\right){\cdot }_s\left(z{-}_{s}w\right)\in {\mathbb{Z}}_s$$
54		oveq12	$$⊢\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\to A{\cdot }_{s}B=\left(x{-}_{s}y\right){\cdot }_s\left(z{-}_{s}w\right)$$
55	54	eleq1d	$$⊢\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\to \left(A{\cdot }_{s}B\in {\mathbb{Z}}_s\leftrightarrow \left(x{-}_{s}y\right){\cdot }_s\left(z{-}_{s}w\right)\in {\mathbb{Z}}_s\right)$$
56	53 55	syl5ibrcom	$$⊢\left(\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\wedge \left(y\in {\mathbb{N}}_s\wedge w\in {\mathbb{N}}_s\right)\right)\to \left(\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\to A{\cdot }_{s}B\in {\mathbb{Z}}_s\right)$$
57	56	rexlimdvva	$$⊢\left(x\in {\mathbb{N}}_s\wedge z\in {\mathbb{N}}_s\right)\to \left(\exists y\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_s\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\to A{\cdot }_{s}B\in {\mathbb{Z}}_s\right)$$
58	57	rexlimivv	$$⊢\exists x\in {\mathbb{N}}_s\exists z\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_s\left(A=x{-}_{s}y\wedge B=z{-}_{s}w\right)\to A{\cdot }_{s}B\in {\mathbb{Z}}_s$$
59	10 58	sylbir	$$⊢\left(\exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\wedge \exists z\in {\mathbb{N}}_s\exists w\in {\mathbb{N}}_{s}B=z{-}_{s}w\right)\to A{\cdot }_{s}B\in {\mathbb{Z}}_s$$
60	4 6 59	syl2anc	$$⊢\phi \to A{\cdot }_{s}B\in {\mathbb{Z}}_s$$