Theorem nnmulcl 9070

Description: Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.)

Assertion

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

Proof of Theorem nnmulcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 5962	. . . . 5 ⊢ (𝑥 = 1 → (𝐴 · 𝑥) = (𝐴 · 1))
2	1	eleq1d 2275	. . . 4 ⊢ (𝑥 = 1 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 1) ∈ ℕ))
3	2	imbi2d 230	. . 3 ⊢ (𝑥 = 1 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ)))
4		oveq2 5962	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦))
5	4	eleq1d 2275	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝑦) ∈ ℕ))
6	5	imbi2d 230	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ)))
7		oveq2 5962	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (𝐴 · 𝑥) = (𝐴 · (𝑦 + 1)))
8	7	eleq1d 2275	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · (𝑦 + 1)) ∈ ℕ))
9	8	imbi2d 230	. . 3 ⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ)))
10		oveq2 5962	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 · 𝑥) = (𝐴 · 𝐵))
11	10	eleq1d 2275	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝐵) ∈ ℕ))
12	11	imbi2d 230	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ)))
13		nncn 9057	. . . 4 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
14		mulrid 8082	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
15	14	eleq1d 2275	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((𝐴 · 1) ∈ ℕ ↔ 𝐴 ∈ ℕ))
16	15	biimprd 158	. . . 4 ⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ))
17	13, 16	mpcom 36	. . 3 ⊢ (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ)
18		nnaddcl 9069	. . . . . . . 8 ⊢ (((𝐴 · 𝑦) ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ)
19	18	ancoms 268	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ)
20		nncn 9057	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
21		ax-1cn 8031	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
22		adddi 8070	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1)))
23	21, 22	mp3an3 1339	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1)))
24	14	oveq2d 5970	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴))
25	24	adantr 276	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴))
26	23, 25	eqtrd 2239	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + 𝐴))
27	13, 20, 26	syl2an 289	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + 𝐴))
28	27	eleq1d 2275	. . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 · (𝑦 + 1)) ∈ ℕ ↔ ((𝐴 · 𝑦) + 𝐴) ∈ ℕ))
29	19, 28	imbitrrid 156	. . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → (𝐴 · (𝑦 + 1)) ∈ ℕ))
30	29	exp4b 367	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))))
31	30	pm2.43b 52	. . . 4 ⊢ (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ)))
32	31	a2d 26	. . 3 ⊢ (𝑦 ∈ ℕ → ((𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ) → (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ)))
33	3, 6, 9, 12, 17, 32	nnind 9065	. 2 ⊢ (𝐵 ∈ ℕ → (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ))
34	33	impcom 125	1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2177  (class class class)co 5954  ℂcc 7936  1c1 7939   + caddc 7941   · cmul 7943  ℕcn 9049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4167  ax-cnex 8029  ax-resscn 8030  ax-1cn 8031  ax-1re 8032  ax-icn 8033  ax-addcl 8034  ax-addrcl 8035  ax-mulcl 8036  ax-mulcom 8039  ax-addass 8040  ax-mulass 8041  ax-distr 8042  ax-1rid 8045  ax-cnre 8049

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-int 3889  df-br 4049  df-iota 5238  df-fv 5285  df-ov 5957  df-inn 9050

This theorem is referenced by:  nnmulcli  9071  nndivtr  9091  nnmulcld  9098  nn0mulcl  9344  qaddcl  9769  qmulcl  9771  modqmulnn  10500  nnexpcl  10710  nnsqcl  10767  faccl  10893  facdiv  10896  faclbnd3  10901  bcrpcl  10911  trirecip  11862  fprodnncl  11971  lcmgcdlem  12449  lcmgcdnn  12454  pcmptcl  12715  pcmpt  12716  4sqlem12  12775  mulgnnass  13543  lgseisenlem1  15597  lgseisenlem2  15598  lgseisenlem3  15599  lgseisenlem4  15600  lgsquadlem1  15604  lgsquadlem2  15605