MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmnn Structured version   Unicode version

Theorem prmnn 14072
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
prmnn  |-  ( P  e.  Prime  ->  P  e.  NN )

Proof of Theorem prmnn
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 isprm 14071 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 460 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   {crab 2818   class class class wbr 4447   2oc2o 7121    ~~ cen 7510   NNcn 10532    || cdivides 13840   Primecprime 14069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-prm 14070
This theorem is referenced by:  prmz  14073  coprm  14093  nprmdvds1  14104  isprm5  14105  prmdvdsexpr  14109  phiprmpw  14158  fermltl  14166  prmdiv  14167  prmdiveq  14168  prmdivdiv  14169  modprm1div  14176  m1dvdsndvds  14177  powm2modprm  14180  reumodprminv  14181  modprm0  14182  nnnn0modprm0  14183  modprmn0modprm0  14184  oddprm  14191  pcpremul  14219  pcdvdsb  14244  pcelnn  14245  pcidlem  14247  pcid  14248  pcdvdstr  14251  pcgcd1  14252  pcprmpw2  14257  pcaddlem  14259  pcadd  14260  pcmptcl  14262  pcmpt  14263  pcmpt2  14264  pcfaclem  14269  pcfac  14270  pcbc  14271  expnprm  14273  prmpwdvds  14274  pockthlem  14275  pockthg  14276  pockthi  14277  prminf  14285  prmreclem4  14289  prmreclem5  14290  prmreclem6  14291  prmrec  14292  1arith  14297  4sqlem11  14325  4sqlem12  14326  4sqlem13  14327  4sqlem14  14328  4sqlem17  14331  4sqlem18  14332  4sqlem19  14333  cshwshashnsame  14439  cshwshash  14440  prmlem1a  14443  pgpfi1  16408  pgp0  16409  sylow1lem1  16411  sylow1lem3  16413  sylow1lem4  16414  sylow1lem5  16415  odcau  16417  pgpfi  16418  fislw  16438  sylow3lem6  16445  gexexlem  16648  prmcyg  16684  ablfac1lem  16906  ablfac1b  16908  ablfac1eu  16911  pgpfac1lem3a  16914  pgpfac1lem3  16915  ablfaclem3  16925  prmirredlem  18287  dfprm2  18288  prmirred  18289  prmirredlemOLD  18290  dfprm2OLD  18291  prmirredOLD  18292  znfld  18363  wilthlem1  23067  wilthlem2  23068  wilthlem3  23069  prmdvdsfi  23106  chtf  23107  efchtcl  23110  vmaval  23112  isppw2  23114  vmappw  23115  vmaprm  23116  vmacl  23117  efvmacl  23119  muval1  23132  chtprm  23152  chtdif  23157  efchtdvds  23158  mumul  23180  sqff1o  23181  dvdsppwf1o  23187  sgmppw  23197  0sgmppw  23198  1sgmprm  23199  vmalelog  23205  chtleppi  23210  chtublem  23211  fsumvma2  23214  vmasum  23216  chpchtsum  23219  chpub  23220  mersenne  23227  perfect1  23228  perfect  23231  pcbcctr  23276  bpos1lem  23282  bposlem1  23284  bposlem2  23285  bposlem6  23289  lgslem1  23296  lgsval2lem  23306  lgsvalmod  23315  lgsmod  23321  lgsdirprm  23329  lgsne0  23333  lgsqrlem1  23341  lgsqrlem2  23342  lgsqrlem4  23344  lgsqr  23346  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisenlem4  23352  lgseisen  23353  lgsquadlem1  23354  lgsquadlem2  23355  lgsquadlem3  23356  lgsquad2lem2  23359  lgsquad2  23360  m1lgs  23362  2sqlem3  23366  2sqlem8  23372  2sqlem11  23375  2sqblem  23377  chtppilimlem1  23383  rplogsumlem2  23395  rpvmasumlem  23397  dchrisum0flblem1  23418  dchrisum0flblem2  23419  dirith2  23438  padicabvf  23541  ostth1  23543  ostth3  23548  hashecclwwlkn1  24507  usghashecclwwlk  24508  hashclwwlkn  24509  clwwlkndivn  24510  clwlkfclwwlk  24517  clwlkfoclwwlk  24518  clwlkf1clwwlk  24523  numclwwlk5  24786  numclwwlk6  24787  numclwwlk7  24788  numclwwlk8  24789  nn0prpwlem  29715  nn0prpw  29716  nzprmdif  30824  ztprmneprm  32000
  Copyright terms: Public domain W3C validator