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

Theorem prmnn 14585
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 14584 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 461 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   {crab 2777   class class class wbr 4417   2oc2o 7175    ~~ cen 7565   NNcn 10598    || cdvds 14272   Primecprime 14582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-prm 14583
This theorem is referenced by:  prmz  14586  prmssnn  14587  nprmdvds1  14610  isprm5  14611  coprm  14617  prmdvdsexpr  14629  phiprmpw  14682  fermltl  14690  prmdiv  14691  prmdiveq  14692  prmdivdiv  14693  modprm1div  14700  m1dvdsndvds  14701  vfermltl  14704  vfermltlALT  14705  powm2modprm  14706  reumodprminv  14707  modprm0  14708  nnnn0modprm0  14709  modprmn0modprm0  14710  oddprm  14717  pcpremul  14745  pcdvdsb  14770  pcelnn  14771  pcidlem  14773  pcid  14774  pcdvdstr  14777  pcgcd1  14778  pcprmpw2  14783  pcaddlem  14785  pcadd  14786  pcmptcl  14788  pcmpt  14789  pcmpt2  14790  pcfaclem  14795  pcfac  14796  pcbc  14797  expnprm  14799  prmpwdvds  14800  pockthlem  14801  pockthg  14802  pockthi  14803  prminf  14811  prmreclem4  14815  prmreclem5  14816  prmreclem6  14817  prmrec  14818  1arith  14823  4sqlem11  14851  4sqlem12  14852  4sqlem13OLD  14853  4sqlem14OLD  14854  4sqlem17OLD  14857  4sqlem18OLD  14858  4sqlem13  14859  4sqlem14  14860  4sqlem17  14863  4sqlem18  14864  4sqlem19  14865  prmdvdsprmo  14952  prmdvdsprmorOLD  14967  prmgaplem3  14975  prmgaplem4  14976  prmgaplem5  14977  prmgaplem6  14978  prmgaplem8  14980  cshwshashnsame  15026  cshwshash  15027  prmlem1a  15030  pgpfi1  17175  pgp0  17176  sylow1lem1  17178  sylow1lem3  17180  sylow1lem4  17181  sylow1lem5  17182  odcau  17184  pgpfi  17185  fislw  17205  sylow3lem6  17212  gexexlem  17418  prmcyg  17456  ablfac1lem  17629  ablfac1b  17631  ablfac1eu  17634  pgpfac1lem3a  17637  pgpfac1lem3  17638  ablfaclem3  17648  prmirredlem  18988  dfprm2  18989  prmirred  18990  znfld  19055  wilthlem1  23855  wilthlem2  23856  wilthlem3  23857  prmdvdsfi  23894  chtf  23895  efchtcl  23898  vmaval  23900  isppw2  23902  vmappw  23903  vmaprm  23904  vmacl  23905  efvmacl  23907  muval1  23920  chtprm  23940  chtdif  23945  efchtdvds  23946  mumul  23968  sqff1o  23969  dvdsppwf1o  23975  sgmppw  23985  0sgmppw  23986  1sgmprm  23987  vmalelog  23993  chtleppi  23998  chtublem  23999  fsumvma2  24002  vmasum  24004  chpchtsum  24007  chpub  24008  mersenne  24015  perfect1  24016  perfect  24019  pcbcctr  24064  bpos1lem  24070  bposlem1  24072  bposlem2  24073  bposlem6  24077  lgslem1  24084  lgsval2lem  24094  lgsvalmod  24103  lgsmod  24109  lgsdirprm  24117  lgsne0  24121  lgsqrlem1  24129  lgsqrlem2  24130  lgsqrlem4  24132  lgsqr  24134  lgseisenlem1  24137  lgseisenlem2  24138  lgseisenlem3  24139  lgseisenlem4  24140  lgseisen  24141  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  lgsquad2lem2  24147  lgsquad2  24148  m1lgs  24150  2sqlem3  24154  2sqlem8  24160  2sqlem11  24163  2sqblem  24165  chtppilimlem1  24171  rplogsumlem2  24183  rpvmasumlem  24185  dchrisum0flblem1  24206  dchrisum0flblem2  24207  dirith2  24226  padicabvf  24329  ostth1  24331  ostth3  24336  hashecclwwlkn1  25404  usghashecclwwlk  25405  hashclwwlkn  25406  clwwlkndivn  25407  clwlkfclwwlk  25414  clwlkfoclwwlk  25415  clwlkf1clwwlk  25420  numclwwlk5  25682  numclwwlk6  25683  numclwwlk7  25684  numclwwlk8  25685  2sqmod  28244  nn0prpwlem  30760  nn0prpw  30761  nzprmdif  36309  etransclem41  37711  etransclem44  37714  etransclem47  37717  etransclem48  37718  perfectALTV  38248  gbepos  38262  gbopos  38263  sgoldbaltlem1  38283  ztprmneprm  38901
  Copyright terms: Public domain W3C validator