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

Theorem prmnn 13778
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 13777 . 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 1756   {crab 2731   class class class wbr 4304   2oc2o 6926    ~~ cen 7319   NNcn 10334    || cdivides 13547   Primecprime 13775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2732  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-prm 13776
This theorem is referenced by:  prmz  13779  coprm  13798  nprmdvds1  13809  isprm5  13810  prmdvdsexpr  13814  phiprmpw  13863  fermltl  13871  prmdiv  13872  prmdiveq  13873  prmdivdiv  13874  modprm1div  13881  reumodprminv  13884  modprm0  13885  nnnn0modprm0  13886  modprmn0modprm0  13887  oddprm  13894  pcpremul  13922  pcdvdsb  13947  pcelnn  13948  pcidlem  13950  pcid  13951  pcdvdstr  13954  pcgcd1  13955  pcprmpw2  13960  pcaddlem  13962  pcadd  13963  pcmptcl  13965  pcmpt  13966  pcmpt2  13967  pcfaclem  13972  pcfac  13973  pcbc  13974  expnprm  13976  prmpwdvds  13977  pockthlem  13978  pockthg  13979  pockthi  13980  prminf  13988  prmreclem4  13992  prmreclem5  13993  prmreclem6  13994  prmrec  13995  1arith  14000  4sqlem11  14028  4sqlem12  14029  4sqlem13  14030  4sqlem14  14031  4sqlem17  14034  4sqlem18  14035  4sqlem19  14036  cshwshashnsame  14142  cshwshash  14143  prmlem1a  14146  pgpfi1  16106  pgp0  16107  sylow1lem1  16109  sylow1lem3  16111  sylow1lem4  16112  sylow1lem5  16113  odcau  16115  pgpfi  16116  fislw  16136  sylow3lem6  16143  gexexlem  16346  prmcyg  16382  ablfac1lem  16581  ablfac1b  16583  ablfac1eu  16586  pgpfac1lem3a  16589  pgpfac1lem3  16590  ablfaclem3  16600  prmirredlem  17929  dfprm2  17930  prmirred  17931  prmirredlemOLD  17932  dfprm2OLD  17933  prmirredOLD  17934  znfld  18005  wilthlem1  22418  wilthlem2  22419  wilthlem3  22420  prmdvdsfi  22457  chtf  22458  efchtcl  22461  vmaval  22463  isppw2  22465  vmappw  22466  vmaprm  22467  vmacl  22468  efvmacl  22470  muval1  22483  chtprm  22503  chtdif  22508  efchtdvds  22509  mumul  22531  sqff1o  22532  dvdsppwf1o  22538  sgmppw  22548  0sgmppw  22549  1sgmprm  22550  vmalelog  22556  chtleppi  22561  chtublem  22562  fsumvma2  22565  vmasum  22567  chpchtsum  22570  chpub  22571  mersenne  22578  perfect1  22579  perfect  22582  pcbcctr  22627  bpos1lem  22633  bposlem1  22635  bposlem2  22636  bposlem6  22640  lgslem1  22647  lgsval2lem  22657  lgsvalmod  22666  lgsmod  22672  lgsdirprm  22680  lgsne0  22684  lgsqrlem1  22692  lgsqrlem2  22693  lgsqrlem4  22695  lgsqr  22697  lgseisenlem1  22700  lgseisenlem2  22701  lgseisenlem3  22702  lgseisenlem4  22703  lgseisen  22704  lgsquadlem1  22705  lgsquadlem2  22706  lgsquadlem3  22707  lgsquad2lem2  22710  lgsquad2  22711  m1lgs  22713  2sqlem3  22717  2sqlem8  22723  2sqlem11  22726  2sqblem  22728  chtppilimlem1  22734  rplogsumlem2  22746  rpvmasumlem  22748  dchrisum0flblem1  22769  dchrisum0flblem2  22770  dirith2  22789  padicabvf  22892  ostth1  22894  ostth3  22899  nn0prpwlem  28529  nn0prpw  28530  m1dvdsndvds  30259  powm2modprm  30260  hashecclwwlkn1  30520  usghashecclwwlk  30521  hashclwwlkn  30522  clwwlkndivn  30523  clwlkfclwwlk  30529  clwlkfoclwwlk  30530  clwlkf1clwwlk  30535  numclwwlk5  30717  numclwwlk6  30718  numclwwlk7  30719  numclwwlk8  30720  ztprmneprm  30751
  Copyright terms: Public domain W3C validator