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