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

Theorem prmnn 12761
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 12760 . 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 1684   {crab 2547   class class class wbr 4023   2oc2o 6473    ~~ cen 6860   NNcn 9746    || cdivides 12531   Primecprime 12758
This theorem is referenced by:  prmz  12762  coprm  12779  nprmdvds1  12790  isprm5  12791  prmdvdsexpr  12795  phiprmpw  12844  fermltl  12852  prmdiv  12853  prmdiveq  12854  prmdivdiv  12855  oddprm  12868  pcpremul  12896  pcdvdsb  12921  pcelnn  12922  pcidlem  12924  pcid  12925  pcdvdstr  12928  pcgcd1  12929  pcprmpw2  12934  pcaddlem  12936  pcadd  12937  pcmptcl  12939  pcmpt  12940  pcmpt2  12941  pcfaclem  12946  pcfac  12947  pcbc  12948  expnprm  12950  prmpwdvds  12951  pockthlem  12952  pockthg  12953  pockthi  12954  prminf  12962  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  prmrec  12969  1arith  12974  4sqlem11  13002  4sqlem12  13003  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  4sqlem18  13009  4sqlem19  13010  prmlem1a  13108  pgpfi1  14906  pgp0  14907  sylow1lem1  14909  sylow1lem3  14911  sylow1lem4  14912  sylow1lem5  14913  odcau  14915  pgpfi  14916  fislw  14936  sylow3lem6  14943  gexexlem  15144  prmcyg  15180  ablfac1lem  15303  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem3a  15311  pgpfac1lem3  15312  ablfaclem3  15322  prmirredlem  16446  dfprm2  16447  prmirred  16448  znfld  16514  wilthlem1  20306  wilthlem2  20307  wilthlem3  20308  prmdvdsfi  20345  chtf  20346  efchtcl  20349  vmaval  20351  isppw2  20353  vmappw  20354  vmaprm  20355  vmacl  20356  vmaf  20357  efvmacl  20358  muval1  20371  chtprm  20391  chtdif  20396  efchtdvds  20397  mumul  20419  sqff1o  20420  dvdsppwf1o  20426  sgmppw  20436  0sgmppw  20437  1sgmprm  20438  vmalelog  20444  chtleppi  20449  chtublem  20450  fsumvma2  20453  vmasum  20455  chpchtsum  20458  chpub  20459  mersenne  20466  perfect1  20467  perfect  20470  pcbcctr  20515  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem6  20528  lgslem1  20535  lgsval2lem  20545  lgsvalmod  20554  lgsmod  20560  lgsdirprm  20568  lgsne0  20572  lgsqrlem1  20580  lgsqrlem2  20581  lgsqrlem4  20583  lgsqr  20585  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem2  20598  lgsquad2  20599  m1lgs  20601  2sqlem3  20605  2sqlem8  20611  2sqlem11  20614  2sqblem  20616  chtppilimlem1  20622  rplogsumlem2  20634  rpvmasumlem  20636  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dirith2  20677  padicabvf  20780  ostth1  20782  ostth3  20787  nn0prpwlem  26238  nn0prpw  26239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-prm 12759
  Copyright terms: Public domain W3C validator