# 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 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\right)\to {A}{B}\in ℕ$

### Proof

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