Metamath Proof Explorer

Theorem nnmcl

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

Ref Expression
Assertion nnmcl ⊢A∈ω∧B∈ω→A⋅𝑜B∈ω

Proof

Step Hyp Ref Expression
1 oveq2 ⊢x=B→A⋅𝑜x=A⋅𝑜B
2 1 eleq1d ⊢x=B→A⋅𝑜x∈ω↔A⋅𝑜B∈ω
3 2 imbi2d ⊢x=B→A∈ω→A⋅𝑜x∈ω↔A∈ω→A⋅𝑜B∈ω
4 oveq2 ⊢x=∅→A⋅𝑜x=A⋅𝑜∅
5 4 eleq1d ⊢x=∅→A⋅𝑜x∈ω↔A⋅𝑜∅∈ω
6 oveq2 ⊢x=y→A⋅𝑜x=A⋅𝑜y
7 6 eleq1d ⊢x=y→A⋅𝑜x∈ω↔A⋅𝑜y∈ω
8 oveq2 ⊢x=suc⁡y→A⋅𝑜x=A⋅𝑜suc⁡y
9 8 eleq1d ⊢x=suc⁡y→A⋅𝑜x∈ω↔A⋅𝑜suc⁡y∈ω
10 nnm0 ⊢A∈ω→A⋅𝑜∅=∅
11 peano1 ⊢∅∈ω
12 10 11 eqeltrdi ⊢A∈ω→A⋅𝑜∅∈ω
13 nnacl ⊢A⋅𝑜y∈ω∧A∈ω→A⋅𝑜y+𝑜A∈ω
14 13 expcom ⊢A∈ω→A⋅𝑜y∈ω→A⋅𝑜y+𝑜A∈ω
15 14 adantr ⊢A∈ω∧y∈ω→A⋅𝑜y∈ω→A⋅𝑜y+𝑜A∈ω
16 nnmsuc ⊢A∈ω∧y∈ω→A⋅𝑜suc⁡y=A⋅𝑜y+𝑜A
17 16 eleq1d ⊢A∈ω∧y∈ω→A⋅𝑜suc⁡y∈ω↔A⋅𝑜y+𝑜A∈ω
18 15 17 sylibrd ⊢A∈ω∧y∈ω→A⋅𝑜y∈ω→A⋅𝑜suc⁡y∈ω
19 18 expcom ⊢y∈ω→A∈ω→A⋅𝑜y∈ω→A⋅𝑜suc⁡y∈ω
20 5 7 9 12 19 finds2 ⊢x∈ω→A∈ω→A⋅𝑜x∈ω
21 3 20 vtoclga ⊢B∈ω→A∈ω→A⋅𝑜B∈ω
22 21 impcom ⊢A∈ω∧B∈ω→A⋅𝑜B∈ω