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

Theorem prmnn 12763
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 12762 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 446 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   {crab 2549   class class class wbr 4025   2oc2o 6475    ~~ cen 6862   NNcn 9748    || cdivides 12533   Primecprime 12760
This theorem is referenced by:  prmz  12764  coprm  12781  nprmdvds1  12792  isprm5  12793  prmdvdsexpr  12797  phiprmpw  12846  fermltl  12854  prmdiv  12855  prmdiveq  12856  prmdivdiv  12857  oddprm  12870  pcpremul  12898  pcdvdsb  12923  pcelnn  12924  pcidlem  12926  pcid  12927  pcdvdstr  12930  pcgcd1  12931  pcprmpw2  12936  pcaddlem  12938  pcadd  12939  pcmptcl  12941  pcmpt  12942  pcmpt2  12943  pcfaclem  12948  pcfac  12949  pcbc  12950  expnprm  12952  prmpwdvds  12953  pockthlem  12954  pockthg  12955  pockthi  12956  prminf  12964  prmreclem4  12968  prmreclem5  12969  prmreclem6  12970  prmrec  12971  1arith  12976  4sqlem11  13004  4sqlem12  13005  4sqlem13  13006  4sqlem14  13007  4sqlem17  13010  4sqlem18  13011  4sqlem19  13012  prmlem1a  13110  pgpfi1  14908  pgp0  14909  sylow1lem1  14911  sylow1lem3  14913  sylow1lem4  14914  sylow1lem5  14915  odcau  14917  pgpfi  14918  fislw  14938  sylow3lem6  14945  gexexlem  15146  prmcyg  15182  ablfac1lem  15305  ablfac1b  15307  ablfac1eu  15310  pgpfac1lem3a  15313  pgpfac1lem3  15314  ablfaclem3  15324  prmirredlem  16448  dfprm2  16449  prmirred  16450  znfld  16516  wilthlem1  20308  wilthlem2  20309  wilthlem3  20310  prmdvdsfi  20347  chtf  20348  efchtcl  20351  vmaval  20353  isppw2  20355  vmappw  20356  vmaprm  20357  vmacl  20358  vmaf  20359  efvmacl  20360  muval1  20373  chtprm  20393  chtdif  20398  efchtdvds  20399  mumul  20421  sqff1o  20422  dvdsppwf1o  20428  sgmppw  20438  0sgmppw  20439  1sgmprm  20440  vmalelog  20446  chtleppi  20451  chtublem  20452  fsumvma2  20455  vmasum  20457  chpchtsum  20460  chpub  20461  mersenne  20468  perfect1  20469  perfect  20472  pcbcctr  20517  bpos1lem  20523  bposlem1  20525  bposlem2  20526  bposlem6  20530  lgslem1  20537  lgsval2lem  20547  lgsvalmod  20556  lgsmod  20562  lgsdirprm  20570  lgsne0  20574  lgsqrlem1  20582  lgsqrlem2  20583  lgsqrlem4  20585  lgsqr  20587  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem3  20592  lgseisenlem4  20593  lgseisen  20594  lgsquadlem1  20595  lgsquadlem2  20596  lgsquadlem3  20597  lgsquad2lem2  20600  lgsquad2  20601  m1lgs  20603  2sqlem3  20607  2sqlem8  20613  2sqlem11  20616  2sqblem  20618  chtppilimlem1  20624  rplogsumlem2  20636  rpvmasumlem  20638  dchrisum0flblem1  20659  dchrisum0flblem2  20660  dirith2  20679  padicabvf  20782  ostth1  20784  ostth3  20789  nn0prpwlem  26249  nn0prpw  26250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-prm 12761
  Copyright terms: Public domain W3C validator