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

Theorem prmnn 12757
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 12756 . 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 1685   {crab 2548   class class class wbr 4024   2oc2o 6469    ~~ cen 6856   NNcn 9742    || cdivides 12527   Primecprime 12754
This theorem is referenced by:  prmz  12758  coprm  12775  nprmdvds1  12786  isprm5  12787  prmdvdsexpr  12791  phiprmpw  12840  fermltl  12848  prmdiv  12849  prmdiveq  12850  prmdivdiv  12851  oddprm  12864  pcpremul  12892  pcdvdsb  12917  pcelnn  12918  pcidlem  12920  pcid  12921  pcdvdstr  12924  pcgcd1  12925  pcprmpw2  12930  pcaddlem  12932  pcadd  12933  pcmptcl  12935  pcmpt  12936  pcmpt2  12937  pcfaclem  12942  pcfac  12943  pcbc  12944  expnprm  12946  prmpwdvds  12947  pockthlem  12948  pockthg  12949  pockthi  12950  prminf  12958  prmreclem4  12962  prmreclem5  12963  prmreclem6  12964  prmrec  12965  1arith  12970  4sqlem11  12998  4sqlem12  12999  4sqlem13  13000  4sqlem14  13001  4sqlem17  13004  4sqlem18  13005  4sqlem19  13006  prmlem1a  13104  pgpfi1  14902  pgp0  14903  sylow1lem1  14905  sylow1lem3  14907  sylow1lem4  14908  sylow1lem5  14909  odcau  14911  pgpfi  14912  fislw  14932  sylow3lem6  14939  gexexlem  15140  prmcyg  15176  ablfac1lem  15299  ablfac1b  15301  ablfac1eu  15304  pgpfac1lem3a  15307  pgpfac1lem3  15308  ablfaclem3  15318  prmirredlem  16442  dfprm2  16443  prmirred  16444  znfld  16510  wilthlem1  20302  wilthlem2  20303  wilthlem3  20304  prmdvdsfi  20341  chtf  20342  efchtcl  20345  vmaval  20347  isppw2  20349  vmappw  20350  vmaprm  20351  vmacl  20352  vmaf  20353  efvmacl  20354  muval1  20367  chtprm  20387  chtdif  20392  efchtdvds  20393  mumul  20415  sqff1o  20416  dvdsppwf1o  20422  sgmppw  20432  0sgmppw  20433  1sgmprm  20434  vmalelog  20440  chtleppi  20445  chtublem  20446  fsumvma2  20449  vmasum  20451  chpchtsum  20454  chpub  20455  mersenne  20462  perfect1  20463  perfect  20466  pcbcctr  20511  bpos1lem  20517  bposlem1  20519  bposlem2  20520  bposlem6  20524  lgslem1  20531  lgsval2lem  20541  lgsvalmod  20550  lgsmod  20556  lgsdirprm  20564  lgsne0  20568  lgsqrlem1  20576  lgsqrlem2  20577  lgsqrlem4  20579  lgsqr  20581  lgseisenlem1  20584  lgseisenlem2  20585  lgseisenlem3  20586  lgseisenlem4  20587  lgseisen  20588  lgsquadlem1  20589  lgsquadlem2  20590  lgsquadlem3  20591  lgsquad2lem2  20594  lgsquad2  20595  m1lgs  20597  2sqlem3  20601  2sqlem8  20607  2sqlem11  20610  2sqblem  20612  chtppilimlem1  20618  rplogsumlem2  20630  rpvmasumlem  20632  dchrisum0flblem1  20653  dchrisum0flblem2  20654  dirith2  20673  padicabvf  20776  ostth1  20778  ostth3  20783  nn0prpwlem  25649  nn0prpw  25650
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ral 2549  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-prm 12755
  Copyright terms: Public domain W3C validator