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

Theorem prmnn 14674
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 14673 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 466 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   {crab 2753   class class class wbr 4416   2oc2o 7202    ~~ cen 7592   NNcn 10637    || cdvds 14354   Primecprime 14671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-prm 14672
This theorem is referenced by:  prmz  14675  prmssnn  14676  nprmdvds1  14699  isprm5  14700  coprm  14706  prmdvdsexpr  14718  phiprmpw  14773  fermltl  14781  prmdiv  14782  prmdiveq  14783  prmdivdiv  14784  modprm1div  14797  m1dvdsndvds  14798  vfermltl  14801  vfermltlALT  14802  powm2modprm  14803  reumodprminv  14804  modprm0  14805  nnnn0modprm0  14806  modprmn0modprm0  14807  oddprm  14814  pcpremul  14842  pcdvdsb  14867  pcelnn  14868  pcidlem  14870  pcid  14871  pcdvdstr  14874  pcgcd1  14875  pcprmpw2  14880  pcaddlem  14882  pcadd  14883  pcmptcl  14885  pcmpt  14886  pcmpt2  14887  pcfaclem  14892  pcfac  14893  pcbc  14894  expnprm  14896  prmpwdvds  14897  pockthlem  14898  pockthg  14899  pockthi  14900  prminf  14908  prmreclem4  14912  prmreclem5  14913  prmreclem6  14914  prmrec  14915  1arith  14920  4sqlem11  14948  4sqlem12  14949  4sqlem13OLD  14950  4sqlem14OLD  14951  4sqlem17OLD  14954  4sqlem18OLD  14955  4sqlem13  14956  4sqlem14  14957  4sqlem17  14960  4sqlem18  14961  4sqlem19  14962  prmdvdsprmo  15049  prmdvdsprmorOLD  15064  prmgaplem3  15072  prmgaplem4  15073  prmgaplem5  15074  prmgaplem6  15075  prmgaplem8  15077  cshwshashnsame  15123  cshwshash  15124  prmlem1a  15127  pgpfi1  17296  pgp0  17297  sylow1lem1  17299  sylow1lem3  17301  sylow1lem4  17302  sylow1lem5  17303  odcau  17305  pgpfi  17306  fislw  17326  sylow3lem6  17333  gexexlem  17539  prmcyg  17577  ablfac1lem  17750  ablfac1b  17752  ablfac1eu  17755  pgpfac1lem3a  17758  pgpfac1lem3  17759  ablfaclem3  17769  prmirredlem  19113  dfprm2  19114  prmirred  19115  znfld  19180  wilthlem1  24042  wilthlem2  24043  wilthlem3  24044  prmdvdsfi  24083  chtf  24084  efchtcl  24087  vmaval  24089  isppw2  24091  vmappw  24092  vmaprm  24093  vmacl  24094  efvmacl  24096  muval1  24109  chtprm  24129  chtdif  24134  efchtdvds  24135  mumul  24157  sqff1o  24158  dvdsppwf1o  24164  sgmppw  24174  0sgmppw  24175  1sgmprm  24176  vmalelog  24182  chtleppi  24187  chtublem  24188  fsumvma2  24191  vmasum  24193  chpchtsum  24196  chpub  24197  mersenne  24204  perfect1  24205  perfect  24208  pcbcctr  24253  bpos1lem  24259  bposlem1  24261  bposlem2  24262  bposlem6  24266  lgslem1  24273  lgsval2lem  24283  lgsvalmod  24292  lgsmod  24298  lgsdirprm  24306  lgsne0  24310  lgsqrlem1  24318  lgsqrlem2  24319  lgsqrlem4  24321  lgsqr  24323  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem3  24328  lgseisenlem4  24329  lgseisen  24330  lgsquadlem1  24331  lgsquadlem2  24332  lgsquadlem3  24333  lgsquad2lem2  24336  lgsquad2  24337  m1lgs  24339  2sqlem3  24343  2sqlem8  24349  2sqlem11  24352  2sqblem  24354  chtppilimlem1  24360  rplogsumlem2  24372  rpvmasumlem  24374  dchrisum0flblem1  24395  dchrisum0flblem2  24396  dirith2  24415  padicabvf  24518  ostth1  24520  ostth3  24525  hashecclwwlkn1  25611  usghashecclwwlk  25612  hashclwwlkn  25613  clwwlkndivn  25614  clwlkfclwwlk  25621  clwlkfoclwwlk  25622  clwlkf1clwwlk  25627  numclwwlk5  25889  numclwwlk6  25890  numclwwlk7  25891  numclwwlk8  25892  2sqmod  28458  nn0prpwlem  31027  nn0prpw  31028  nzprmdif  36712  etransclem41  38178  etransclem44  38181  etransclem47  38184  etransclem48OLD  38185  etransclem48  38186  perfectALTV  38883  gbepos  38897  gbopos  38898  sgoldbaltlem1  38918  ztprmneprm  40401
  Copyright terms: Public domain W3C validator