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