# Metamath Proof Explorer

## Theorem nnmcl

Description: Closure of multiplication of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnmcl ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{B}\in \mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}={B}\to {A}{\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}{B}$
2 1 eleq1d ${⊢}{x}={B}\to \left({A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }↔{A}{\cdot }_{𝑜}{B}\in \mathrm{\omega }\right)$
3 2 imbi2d ${⊢}{x}={B}\to \left(\left({A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }\right)↔\left({A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}{B}\in \mathrm{\omega }\right)\right)$
4 oveq2 ${⊢}{x}=\varnothing \to {A}{\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\varnothing$
5 4 eleq1d ${⊢}{x}=\varnothing \to \left({A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }↔{A}{\cdot }_{𝑜}\varnothing \in \mathrm{\omega }\right)$
6 oveq2 ${⊢}{x}={y}\to {A}{\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}{y}$
7 6 eleq1d ${⊢}{x}={y}\to \left({A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }↔{A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\right)$
8 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {A}{\cdot }_{𝑜}{x}={A}{\cdot }_{𝑜}\mathrm{suc}{y}$
9 8 eleq1d ${⊢}{x}=\mathrm{suc}{y}\to \left({A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }↔{A}{\cdot }_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)$
10 nnm0 ${⊢}{A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}\varnothing =\varnothing$
11 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
12 10 11 eqeltrdi ${⊢}{A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}\varnothing \in \mathrm{\omega }$
13 nnacl ${⊢}\left({A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\wedge {A}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{A}\in \mathrm{\omega }$
14 13 expcom ${⊢}{A}\in \mathrm{\omega }\to \left({A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\to \left({A}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{A}\in \mathrm{\omega }\right)$
15 14 adantr ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\to \left({A}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{A}\in \mathrm{\omega }\right)$
16 nnmsuc ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{suc}{y}=\left({A}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{A}$
17 16 eleq1d ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }↔\left({A}{\cdot }_{𝑜}{y}\right){+}_{𝑜}{A}\in \mathrm{\omega }\right)$
18 15 17 sylibrd ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to \left({A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)$
19 18 expcom ${⊢}{y}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to \left({A}{\cdot }_{𝑜}{y}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)\right)$
20 5 7 9 12 19 finds2 ${⊢}{x}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }\right)$
21 3 20 vtoclga ${⊢}{B}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to {A}{\cdot }_{𝑜}{B}\in \mathrm{\omega }\right)$
22 21 impcom ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{B}\in \mathrm{\omega }$