![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnmulcl | Structured version Visualization version GIF version |
Description: Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11115 and ax-mulass 11117. (Revised by Steven Nguyen, 24-Sep-2022.) |
Ref | Expression |
---|---|
nnmulcl | ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 7365 | . . . . 5 ⊢ (𝑥 = 1 → (𝐴 · 𝑥) = (𝐴 · 1)) | |
2 | 1 | eleq1d 2822 | . . . 4 ⊢ (𝑥 = 1 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 1) ∈ ℕ)) |
3 | 2 | imbi2d 340 | . . 3 ⊢ (𝑥 = 1 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ))) |
4 | oveq2 7365 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) | |
5 | 4 | eleq1d 2822 | . . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝑦) ∈ ℕ)) |
6 | 5 | imbi2d 340 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ))) |
7 | oveq2 7365 | . . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (𝐴 · 𝑥) = (𝐴 · (𝑦 + 1))) | |
8 | 7 | eleq1d 2822 | . . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · (𝑦 + 1)) ∈ ℕ)) |
9 | 8 | imbi2d 340 | . . 3 ⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
10 | oveq2 7365 | . . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 · 𝑥) = (𝐴 · 𝐵)) | |
11 | 10 | eleq1d 2822 | . . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝐵) ∈ ℕ)) |
12 | 11 | imbi2d 340 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ))) |
13 | nnre 12160 | . . . 4 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ) | |
14 | ax-1rid 11121 | . . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | |
15 | 14 | eleq1d 2822 | . . . . 5 ⊢ (𝐴 ∈ ℝ → ((𝐴 · 1) ∈ ℕ ↔ 𝐴 ∈ ℕ)) |
16 | 15 | biimprd 247 | . . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ)) |
17 | 13, 16 | mpcom 38 | . . 3 ⊢ (𝐴 ∈ ℕ → (𝐴 · 1) ∈ ℕ) |
18 | nnaddcl 12176 | . . . . . . . 8 ⊢ (((𝐴 · 𝑦) ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ) | |
19 | 18 | ancoms 459 | . . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ) |
20 | nncn 12161 | . . . . . . . . . 10 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | |
21 | nncn 12161 | . . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℂ) | |
22 | ax-1cn 11109 | . . . . . . . . . . 11 ⊢ 1 ∈ ℂ | |
23 | adddi 11140 | . . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) | |
24 | 22, 23 | mp3an3 1450 | . . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) |
25 | 20, 21, 24 | syl2an 596 | . . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) |
26 | 13, 14 | syl 17 | . . . . . . . . . . 11 ⊢ (𝐴 ∈ ℕ → (𝐴 · 1) = 𝐴) |
27 | 26 | adantr 481 | . . . . . . . . . 10 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝐴 · 1) = 𝐴) |
28 | 27 | oveq2d 7373 | . . . . . . . . 9 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴)) |
29 | 25, 28 | eqtrd 2776 | . . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + 𝐴)) |
30 | 29 | eleq1d 2822 | . . . . . . 7 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 · (𝑦 + 1)) ∈ ℕ ↔ ((𝐴 · 𝑦) + 𝐴) ∈ ℕ)) |
31 | 19, 30 | syl5ibr 245 | . . . . . 6 ⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → (𝐴 · (𝑦 + 1)) ∈ ℕ)) |
32 | 31 | exp4b 431 | . . . . 5 ⊢ (𝐴 ∈ ℕ → (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ)))) |
33 | 32 | pm2.43b 55 | . . . 4 ⊢ (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
34 | 33 | a2d 29 | . . 3 ⊢ (𝑦 ∈ ℕ → ((𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ) → (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
35 | 3, 6, 9, 12, 17, 34 | nnind 12171 | . 2 ⊢ (𝐵 ∈ ℕ → (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ)) |
36 | 35 | impcom 408 | 1 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 (class class class)co 7357 ℂcc 11049 ℝcr 11050 1c1 11052 + caddc 11054 · cmul 11056 ℕcn 12153 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7672 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-addass 11116 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rrecex 11123 ax-cnre 11124 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-om 7803 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-nn 12154 |
This theorem is referenced by: nnmulcli 12178 nnmtmip 12179 nndivtr 12200 nnmulcld 12206 nn0mulcl 12449 qaddcl 12890 qmulcl 12892 modmulnn 13794 nnexpcl 13980 nnsqcl 14033 expmulnbnd 14138 faccl 14183 facdiv 14187 faclbnd3 14192 faclbnd4lem3 14195 faclbnd5 14198 bcrpcl 14208 trirecip 15748 fprodnncl 15838 nnrisefaccl 15902 lcmgcdlem 16482 lcmgcdnn 16487 pcmptcl 16763 prmreclem1 16788 prmreclem6 16793 4sqlem12 16828 vdwlem3 16855 vdwlem9 16861 vdwlem10 16862 mulgnnass 18911 ovolunlem1a 24860 ovolunlem1 24861 mbfi1fseqlem3 25082 mbfi1fseqlem4 25083 elqaalem2 25680 elqaalem3 25681 log2cnv 26294 log2tlbnd 26295 log2ublem2 26297 log2ub 26299 basellem1 26430 basellem2 26431 basellem3 26432 basellem4 26433 basellem5 26434 basellem6 26435 basellem7 26436 basellem8 26437 basellem9 26438 efnnfsumcl 26452 efchtdvds 26508 mumullem1 26528 mumullem2 26529 fsumdvdscom 26534 dvdsflf1o 26536 chtublem 26559 pcbcctr 26624 bclbnd 26628 bposlem1 26632 bposlem2 26633 bposlem3 26634 bposlem4 26635 bposlem5 26636 bposlem6 26637 lgseisenlem1 26723 lgseisenlem2 26724 lgseisenlem3 26725 lgseisenlem4 26726 lgsquadlem1 26728 lgsquadlem2 26729 chebbnd1lem1 26817 chebbnd1lem3 26819 dchrisumlem1 26837 mulogsum 26880 pntrsumo1 26913 pntrsumbnd 26914 ostth2lem1 26966 subfaclim 33782 jm2.17a 41270 jm2.17b 41271 jm2.17c 41272 acongrep 41290 acongeq 41293 jm2.27a 41315 jm2.27c 41317 |
Copyright terms: Public domain | W3C validator |