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

Theorem prmnn 13762
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 13761 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 457 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   {crab 2717   class class class wbr 4289   2oc2o 6910    ~~ cen 7303   NNcn 10318    || cdivides 13531   Primecprime 13759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-prm 13760
This theorem is referenced by:  prmz  13763  coprm  13782  nprmdvds1  13793  isprm5  13794  prmdvdsexpr  13798  phiprmpw  13847  fermltl  13855  prmdiv  13856  prmdiveq  13857  prmdivdiv  13858  modprm1div  13865  reumodprminv  13868  modprm0  13869  nnnn0modprm0  13870  modprmn0modprm0  13871  oddprm  13878  pcpremul  13906  pcdvdsb  13931  pcelnn  13932  pcidlem  13934  pcid  13935  pcdvdstr  13938  pcgcd1  13939  pcprmpw2  13944  pcaddlem  13946  pcadd  13947  pcmptcl  13949  pcmpt  13950  pcmpt2  13951  pcfaclem  13956  pcfac  13957  pcbc  13958  expnprm  13960  prmpwdvds  13961  pockthlem  13962  pockthg  13963  pockthi  13964  prminf  13972  prmreclem4  13976  prmreclem5  13977  prmreclem6  13978  prmrec  13979  1arith  13984  4sqlem11  14012  4sqlem12  14013  4sqlem13  14014  4sqlem14  14015  4sqlem17  14018  4sqlem18  14019  4sqlem19  14020  cshwshashnsame  14126  cshwshash  14127  prmlem1a  14130  pgpfi1  16087  pgp0  16088  sylow1lem1  16090  sylow1lem3  16092  sylow1lem4  16093  sylow1lem5  16094  odcau  16096  pgpfi  16097  fislw  16117  sylow3lem6  16124  gexexlem  16327  prmcyg  16363  ablfac1lem  16559  ablfac1b  16561  ablfac1eu  16564  pgpfac1lem3a  16567  pgpfac1lem3  16568  ablfaclem3  16578  prmirredlem  17876  dfprm2  17877  prmirred  17878  prmirredlemOLD  17879  dfprm2OLD  17880  prmirredOLD  17881  znfld  17952  wilthlem1  22365  wilthlem2  22366  wilthlem3  22367  prmdvdsfi  22404  chtf  22405  efchtcl  22408  vmaval  22410  isppw2  22412  vmappw  22413  vmaprm  22414  vmacl  22415  efvmacl  22417  muval1  22430  chtprm  22450  chtdif  22455  efchtdvds  22456  mumul  22478  sqff1o  22479  dvdsppwf1o  22485  sgmppw  22495  0sgmppw  22496  1sgmprm  22497  vmalelog  22503  chtleppi  22508  chtublem  22509  fsumvma2  22512  vmasum  22514  chpchtsum  22517  chpub  22518  mersenne  22525  perfect1  22526  perfect  22529  pcbcctr  22574  bpos1lem  22580  bposlem1  22582  bposlem2  22583  bposlem6  22587  lgslem1  22594  lgsval2lem  22604  lgsvalmod  22613  lgsmod  22619  lgsdirprm  22627  lgsne0  22631  lgsqrlem1  22639  lgsqrlem2  22640  lgsqrlem4  22642  lgsqr  22644  lgseisenlem1  22647  lgseisenlem2  22648  lgseisenlem3  22649  lgseisenlem4  22650  lgseisen  22651  lgsquadlem1  22652  lgsquadlem2  22653  lgsquadlem3  22654  lgsquad2lem2  22657  lgsquad2  22658  m1lgs  22660  2sqlem3  22664  2sqlem8  22670  2sqlem11  22673  2sqblem  22675  chtppilimlem1  22681  rplogsumlem2  22693  rpvmasumlem  22695  dchrisum0flblem1  22716  dchrisum0flblem2  22717  dirith2  22736  padicabvf  22839  ostth1  22841  ostth3  22846  nn0prpwlem  28442  nn0prpw  28443  m1dvdsndvds  30172  powm2modprm  30173  hashecclwwlkn1  30433  usghashecclwwlk  30434  hashclwwlkn  30435  clwwlkndivn  30436  clwlkfclwwlk  30442  clwlkfoclwwlk  30443  clwlkf1clwwlk  30448  numclwwlk5  30630  numclwwlk6  30631  numclwwlk7  30632  numclwwlk8  30633  ztprmneprm  30663
  Copyright terms: Public domain W3C validator