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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) ∈ ω )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐵 ) )
2 1 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ·o 𝑥 ) ∈ ω ↔ ( 𝐴 ·o 𝐵 ) ∈ ω ) )
3 2 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 ·o 𝑥 ) ∈ ω ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ·o 𝐵 ) ∈ ω ) ) )
4 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
5 4 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝑥 ) ∈ ω ↔ ( 𝐴 ·o ∅ ) ∈ ω ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
7 6 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ ω ↔ ( 𝐴 ·o 𝑦 ) ∈ ω ) )
8 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
9 8 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ ω ↔ ( 𝐴 ·o suc 𝑦 ) ∈ ω ) )
10 nnm0 ⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o ∅ ) = ∅ )
11 peano1 ⊢ ∅ ∈ ω
12 10 11 eqeltrdi ⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o ∅ ) ∈ ω )
13 nnacl ⊢ ( ( ( 𝐴 ·o 𝑦 ) ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ω )
14 13 expcom ⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ·o 𝑦 ) ∈ ω → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ω ) )
15 14 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o 𝑦 ) ∈ ω → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ω ) )
16 nnmsuc ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
17 16 eleq1d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o suc 𝑦 ) ∈ ω ↔ ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ ω ) )
18 15 17 sylibrd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ·o 𝑦 ) ∈ ω → ( 𝐴 ·o suc 𝑦 ) ∈ ω ) )
19 18 expcom ⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 ·o 𝑦 ) ∈ ω → ( 𝐴 ·o suc 𝑦 ) ∈ ω ) ) )
20 5 7 9 12 19 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ·o 𝑥 ) ∈ ω ) )
21 3 20 vtoclga ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ·o 𝐵 ) ∈ ω ) )
22 21 impcom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) ∈ ω )