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 imbitrrid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 ∈ ℕ ∧ ( 𝐴 · 𝑦 ) ∈ ℕ ) → ( 𝐴 · ( 𝑦 + 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 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )