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

Theorem prmnn 12777
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 12776 . 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 1696   {crab 2560   class class class wbr 4039   2oc2o 6489    ~~ cen 6876   NNcn 9762    || cdivides 12547   Primecprime 12774
This theorem is referenced by:  prmz  12778  coprm  12795  nprmdvds1  12806  isprm5  12807  prmdvdsexpr  12811  phiprmpw  12860  fermltl  12868  prmdiv  12869  prmdiveq  12870  prmdivdiv  12871  oddprm  12884  pcpremul  12912  pcdvdsb  12937  pcelnn  12938  pcidlem  12940  pcid  12941  pcdvdstr  12944  pcgcd1  12945  pcprmpw2  12950  pcaddlem  12952  pcadd  12953  pcmptcl  12955  pcmpt  12956  pcmpt2  12957  pcfaclem  12962  pcfac  12963  pcbc  12964  expnprm  12966  prmpwdvds  12967  pockthlem  12968  pockthg  12969  pockthi  12970  prminf  12978  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  prmrec  12985  1arith  12990  4sqlem11  13018  4sqlem12  13019  4sqlem13  13020  4sqlem14  13021  4sqlem17  13024  4sqlem18  13025  4sqlem19  13026  prmlem1a  13124  pgpfi1  14922  pgp0  14923  sylow1lem1  14925  sylow1lem3  14927  sylow1lem4  14928  sylow1lem5  14929  odcau  14931  pgpfi  14932  fislw  14952  sylow3lem6  14959  gexexlem  15160  prmcyg  15196  ablfac1lem  15319  ablfac1b  15321  ablfac1eu  15324  pgpfac1lem3a  15327  pgpfac1lem3  15328  ablfaclem3  15338  prmirredlem  16462  dfprm2  16463  prmirred  16464  znfld  16530  wilthlem1  20322  wilthlem2  20323  wilthlem3  20324  prmdvdsfi  20361  chtf  20362  efchtcl  20365  vmaval  20367  isppw2  20369  vmappw  20370  vmaprm  20371  vmacl  20372  vmaf  20373  efvmacl  20374  muval1  20387  chtprm  20407  chtdif  20412  efchtdvds  20413  mumul  20435  sqff1o  20436  dvdsppwf1o  20442  sgmppw  20452  0sgmppw  20453  1sgmprm  20454  vmalelog  20460  chtleppi  20465  chtublem  20466  fsumvma2  20469  vmasum  20471  chpchtsum  20474  chpub  20475  mersenne  20482  perfect1  20483  perfect  20486  pcbcctr  20531  bpos1lem  20537  bposlem1  20539  bposlem2  20540  bposlem6  20544  lgslem1  20551  lgsval2lem  20561  lgsvalmod  20570  lgsmod  20576  lgsdirprm  20584  lgsne0  20588  lgsqrlem1  20596  lgsqrlem2  20597  lgsqrlem4  20599  lgsqr  20601  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2lem2  20614  lgsquad2  20615  m1lgs  20617  2sqlem3  20621  2sqlem8  20627  2sqlem11  20630  2sqblem  20632  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasumlem  20652  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dirith2  20693  padicabvf  20796  ostth1  20798  ostth3  20803  nn0prpwlem  26341  nn0prpw  26342
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-prm 12775
  Copyright terms: Public domain W3C validator