Theorem nnmulscl

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

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

Proof

Step	Hyp	Ref	Expression
1		n0mulscl	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s ) → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s )
2	1	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → ( 𝐴 ·s 𝐵 ) ∈ ℕ0s )
3		simpll	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 𝐴 ∈ ℕ0s )
4	3	n0snod	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 𝐴 ∈ No )
5		simprl	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 𝐵 ∈ ℕ0s )
6	5	n0snod	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 𝐵 ∈ No )
7		simplr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 0s <s 𝐴 )
8		simprr	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 0s <s 𝐵 )
9	4 6 7 8	mulsgt0d	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → 0s <s ( 𝐴 ·s 𝐵 ) )
10	2 9	jca	⊢ ( ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ ℕ0s ∧ 0s <s ( 𝐴 ·s 𝐵 ) ) )
11		elnns2	⊢ ( 𝐴 ∈ ℕs ↔ ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) )
12		elnns2	⊢ ( 𝐵 ∈ ℕs ↔ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) )
13	11 12	anbi12i	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ) ↔ ( ( 𝐴 ∈ ℕ0s ∧ 0s <s 𝐴 ) ∧ ( 𝐵 ∈ ℕ0s ∧ 0s <s 𝐵 ) ) )
14		elnns2	⊢ ( ( 𝐴 ·s 𝐵 ) ∈ ℕs ↔ ( ( 𝐴 ·s 𝐵 ) ∈ ℕ0s ∧ 0s <s ( 𝐴 ·s 𝐵 ) ) )
15	10 13 14	3imtr4i	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ) → ( 𝐴 ·s 𝐵 ) ∈ ℕs )