# Metamath Proof Explorer

## Theorem nnmulcl

Description: Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997) Remove dependency on ax-mulcom and ax-mulass . (Revised by Steven Nguyen, 24-Sep-2022)

Ref Expression
Assertion nnmulcl ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )

### Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = 1 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 1 ) )
2 1 eleq1d ( 𝑥 = 1 → ( ( 𝐴 · 𝑥 ) ∈ ℕ ↔ ( 𝐴 · 1 ) ∈ ℕ ) )
3 2 imbi2d ( 𝑥 = 1 → ( ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑥 ) ∈ ℕ ) ↔ ( 𝐴 ∈ ℕ → ( 𝐴 · 1 ) ∈ ℕ ) ) )
4 oveq2 ( 𝑥 = 𝑦 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑦 ) )
5 4 eleq1d ( 𝑥 = 𝑦 → ( ( 𝐴 · 𝑥 ) ∈ ℕ ↔ ( 𝐴 · 𝑦 ) ∈ ℕ ) )
6 5 imbi2d ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑥 ) ∈ ℕ ) ↔ ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑦 ) ∈ ℕ ) ) )
7 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( 𝑦 + 1 ) ) )
8 7 eleq1d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 · 𝑥 ) ∈ ℕ ↔ ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) )
9 8 imbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑥 ) ∈ ℕ ) ↔ ( 𝐴 ∈ ℕ → ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) ) )
10 oveq2 ( 𝑥 = 𝐵 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝐵 ) )
11 10 eleq1d ( 𝑥 = 𝐵 → ( ( 𝐴 · 𝑥 ) ∈ ℕ ↔ ( 𝐴 · 𝐵 ) ∈ ℕ ) )
12 11 imbi2d ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑥 ) ∈ ℕ ) ↔ ( 𝐴 ∈ ℕ → ( 𝐴 · 𝐵 ) ∈ ℕ ) ) )
13 nnre ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
14 ax-1rid ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
15 14 eleq1d ( 𝐴 ∈ ℝ → ( ( 𝐴 · 1 ) ∈ ℕ ↔ 𝐴 ∈ ℕ ) )
16 15 biimprd ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℕ → ( 𝐴 · 1 ) ∈ ℕ ) )
17 13 16 mpcom ( 𝐴 ∈ ℕ → ( 𝐴 · 1 ) ∈ ℕ )
18 nnaddcl ( ( ( 𝐴 · 𝑦 ) ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( ( 𝐴 · 𝑦 ) + 𝐴 ) ∈ ℕ )
19 18 ancoms ( ( 𝐴 ∈ ℕ ∧ ( 𝐴 · 𝑦 ) ∈ ℕ ) → ( ( 𝐴 · 𝑦 ) + 𝐴 ) ∈ ℕ )
20 nncn ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
21 nncn ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
22 ax-1cn 1 ∈ ℂ
23 adddi ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 · ( 𝑦 + 1 ) ) = ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) )
24 22 23 mp3an3 ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · ( 𝑦 + 1 ) ) = ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) )
25 20 21 24 syl2an ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 · ( 𝑦 + 1 ) ) = ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) )
26 13 14 syl ( 𝐴 ∈ ℕ → ( 𝐴 · 1 ) = 𝐴 )
27 26 adantr ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 · 1 ) = 𝐴 )
28 27 oveq2d ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 · 𝑦 ) + ( 𝐴 · 1 ) ) = ( ( 𝐴 · 𝑦 ) + 𝐴 ) )
29 25 28 eqtrd ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 · ( 𝑦 + 1 ) ) = ( ( 𝐴 · 𝑦 ) + 𝐴 ) )
30 29 eleq1d ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ↔ ( ( 𝐴 · 𝑦 ) + 𝐴 ) ∈ ℕ ) )
31 19 30 syl5ibr ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 ∈ ℕ ∧ ( 𝐴 · 𝑦 ) ∈ ℕ ) → ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) )
32 31 exp4b ( 𝐴 ∈ ℕ → ( 𝑦 ∈ ℕ → ( 𝐴 ∈ ℕ → ( ( 𝐴 · 𝑦 ) ∈ ℕ → ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) ) ) )
33 32 pm2.43b ( 𝑦 ∈ ℕ → ( 𝐴 ∈ ℕ → ( ( 𝐴 · 𝑦 ) ∈ ℕ → ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) ) )
34 33 a2d ( 𝑦 ∈ ℕ → ( ( 𝐴 ∈ ℕ → ( 𝐴 · 𝑦 ) ∈ ℕ ) → ( 𝐴 ∈ ℕ → ( 𝐴 · ( 𝑦 + 1 ) ) ∈ ℕ ) ) )
35 3 6 9 12 17 34 nnind ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ℕ → ( 𝐴 · 𝐵 ) ∈ ℕ ) )
36 35 impcom ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )