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 ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ⁢ B ∈ ℕ

Proof

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