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∈𝑵