Theorem n0mulscl

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

	Ref	Expression
Assertion	n0mulscl	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s ) → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 0s → ( 𝐴 ·s 𝑛 ) = ( 𝐴 ·s 0s ) )
2	1	eleq1d	⊢ ( 𝑛 = 0s → ( ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 ·s 0s ) ∈ ℕ0s ) )
3	2	imbi2d	⊢ ( 𝑛 = 0s → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 0s ) ∈ ℕ0s ) ) )
4		oveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐴 ·s 𝑛 ) = ( 𝐴 ·s 𝑚 ) )
5	4	eleq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) )
6	5	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) ) )
7		oveq2	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( 𝐴 ·s 𝑛 ) = ( 𝐴 ·s ( 𝑚 +s 1s ) ) )
8	7	eleq1d	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) )
9	8	imbi2d	⊢ ( 𝑛 = ( 𝑚 +s 1s ) → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
10		oveq2	⊢ ( 𝑛 = 𝐵 → ( 𝐴 ·s 𝑛 ) = ( 𝐴 ·s 𝐵 ) )
11	10	eleq1d	⊢ ( 𝑛 = 𝐵 → ( ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ↔ ( 𝐴 ·s 𝐵 ) ∈ ℕ0s ) )
12	11	imbi2d	⊢ ( 𝑛 = 𝐵 → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑛 ) ∈ ℕ0s ) ↔ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s ) ) )
13		n0sno	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
14		muls01	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
15	13 14	syl	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 0s ) = 0s )
16		0n0s	⊢ 0s ∈ ℕ0s
17	15 16	eqeltrdi	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 0s ) ∈ ℕ0s )
18	13	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → 𝐴 ∈ No )
19		n0sno	⊢ ( 𝑚 ∈ ℕ0s → 𝑚 ∈ No )
20	19	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → 𝑚 ∈ No )
21		1sno	⊢ 1s ∈ No
22	21	a1i	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → 1s ∈ No )
23	18 20 22	addsdid	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 ·s ( 𝑚 +s 1s ) ) = ( ( 𝐴 ·s 𝑚 ) +s ( 𝐴 ·s 1s ) ) )
24	13	mulsridd	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 1s ) = 𝐴 )
25	24	oveq2d	⊢ ( 𝐴 ∈ ℕ0s → ( ( 𝐴 ·s 𝑚 ) +s ( 𝐴 ·s 1s ) ) = ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) )
26	25	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( ( 𝐴 ·s 𝑚 ) +s ( 𝐴 ·s 1s ) ) = ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) )
27	23 26	eqtrd	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 ·s ( 𝑚 +s 1s ) ) = ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) )
28		n0addscl	⊢ ( ( ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ∧ 𝐴 ∈ ℕ0s ) → ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) ∈ ℕ0s )
29	28	ancoms	⊢ ( ( 𝐴 ∈ ℕ0s ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) ∈ ℕ0s )
30	29	adantlr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( ( 𝐴 ·s 𝑚 ) +s 𝐴 ) ∈ ℕ0s )
31	27 30	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) ∧ ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s )
32	31	ex	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑚 ∈ ℕ0s ) → ( ( 𝐴 ·s 𝑚 ) ∈ ℕ0s → ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) )
33	32	expcom	⊢ ( 𝑚 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( ( 𝐴 ·s 𝑚 ) ∈ ℕ0s → ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
34	33	a2d	⊢ ( 𝑚 ∈ ℕ0s → ( ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝑚 ) ∈ ℕ0s ) → ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s ( 𝑚 +s 1s ) ) ∈ ℕ0s ) ) )
35	3 6 9 12 17 34	n0sind	⊢ ( 𝐵 ∈ ℕ0s → ( 𝐴 ∈ ℕ0s → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s ) )
36	35	impcom	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s ) → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s )