Metamath Proof Explorer

Theorem nnmulscl

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

Ref Expression
Assertion nnmulscl ⊢ A ∈ ℕ s ∧ B ∈ ℕ s → A ⋅ s B ∈ ℕ s

Proof

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