![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnmulcld | Structured version Visualization version GIF version |
Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnge1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
nnmulcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℕ) |
Ref | Expression |
---|---|
nnmulcld | ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnge1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
2 | nnmulcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℕ) | |
3 | nnmulcl 11462 | . 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) | |
4 | 1, 2, 3 | syl2anc 576 | 1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 (class class class)co 6974 · cmul 10338 ℕcn 11437 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-addass 10398 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rrecex 10405 ax-cnre 10406 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-om 7395 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-nn 11438 |
This theorem is referenced by: bcm1k 13488 bcp1n 13489 permnn 13499 trireciplem 15075 efaddlem 15304 eftlub 15320 eirrlem 15415 modmulconst 15499 isprm5 15905 crth 15969 phimullem 15970 pcqmul 16044 pcaddlem 16078 pcbc 16090 oddprmdvds 16093 pockthlem 16095 pockthg 16096 vdwlem3 16173 vdwlem6 16176 vdwlem9 16179 torsubg 18742 ablfacrp 18950 dgrcolem1 24578 aalioulem5 24640 aaliou3lem2 24647 log2cnv 25236 log2tlbnd 25237 log2ublem2 25239 log2ub 25241 lgamgulmlem4 25323 wilthlem2 25360 ftalem7 25370 basellem5 25376 mumul 25472 fsumfldivdiaglem 25480 dvdsmulf1o 25485 sgmmul 25491 chtublem 25501 bcmono 25567 bposlem3 25576 bposlem5 25578 gausslemma2dlem1a 25655 lgsquadlem2 25671 lgsquadlem3 25672 lgsquad2lem2 25675 2sqlem6 25713 2sqmod 25726 rplogsumlem1 25774 rplogsumlem2 25775 dchrisum0fmul 25796 vmalogdivsum2 25828 pntrsumbnd2 25857 pntpbnd1 25876 pntpbnd2 25877 ostth2lem2 25924 oddpwdc 31286 eulerpartlemgh 31310 subfaclim 32049 bcprod 32519 faclim2 32529 jm2.27c 39029 relexpmulnn 39446 mccllem 41334 limsup10exlem 41509 wallispilem5 41810 wallispi2lem1 41812 wallispi2 41814 stirlinglem3 41817 stirlinglem8 41822 stirlinglem15 41829 dirkertrigeqlem3 41841 hoicvrrex 42294 deccarry 42942 fmtnoprmfac2 43122 sfprmdvdsmersenne 43161 lighneallem3 43165 proththdlem 43171 fppr2odd 43289 blennnt2 44042 |
Copyright terms: Public domain | W3C validator |