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∈ℕ