Metamath Proof Explorer

Theorem mulclpi

Description: Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion mulclpi ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B ∈ 𝑵

Proof

Step Hyp Ref Expression
1 mulpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑜 B
2 pinn ⊢ A ∈ 𝑵 → A ∈ ω
3 pinn ⊢ B ∈ 𝑵 → B ∈ ω
4 nnmcl ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ∈ ω
5 2 3 4 syl2an ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑜 B ∈ ω
6 elni2 ⊢ B ∈ 𝑵 ↔ B ∈ ω ∧ ∅ ∈ B
7 6 simprbi ⊢ B ∈ 𝑵 → ∅ ∈ B
8 7 adantl ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ∅ ∈ B
9 3 adantl ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → B ∈ ω
10 2 adantr ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ∈ ω
11 elni2 ⊢ A ∈ 𝑵 ↔ A ∈ ω ∧ ∅ ∈ A
12 11 simprbi ⊢ A ∈ 𝑵 → ∅ ∈ A
13 12 adantr ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ∅ ∈ A
14 nnmordi ⊢ B ∈ ω ∧ A ∈ ω ∧ ∅ ∈ A → ∅ ∈ B → A ⋅ 𝑜 ∅ ∈ A ⋅ 𝑜 B
15 9 10 13 14 syl21anc ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ∅ ∈ B → A ⋅ 𝑜 ∅ ∈ A ⋅ 𝑜 B
16 8 15 mpd ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑜 ∅ ∈ A ⋅ 𝑜 B
17 16 ne0d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑜 B ≠ ∅
18 elni ⊢ A ⋅ 𝑜 B ∈ 𝑵 ↔ A ⋅ 𝑜 B ∈ ω ∧ A ⋅ 𝑜 B ≠ ∅
19 5 17 18 sylanbrc ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑜 B ∈ 𝑵
20 1 19 eqeltrd ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B ∈ 𝑵