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 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 ω