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

Theorem prmnn 13037
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 13036 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 447 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   {crab 2670   class class class wbr 4172   2oc2o 6677    ~~ cen 7065   NNcn 9956    || cdivides 12807   Primecprime 13034
This theorem is referenced by:  prmz  13038  coprm  13055  nprmdvds1  13066  isprm5  13067  prmdvdsexpr  13071  phiprmpw  13120  fermltl  13128  prmdiv  13129  prmdiveq  13130  prmdivdiv  13131  oddprm  13144  pcpremul  13172  pcdvdsb  13197  pcelnn  13198  pcidlem  13200  pcid  13201  pcdvdstr  13204  pcgcd1  13205  pcprmpw2  13210  pcaddlem  13212  pcadd  13213  pcmptcl  13215  pcmpt  13216  pcmpt2  13217  pcfaclem  13222  pcfac  13223  pcbc  13224  expnprm  13226  prmpwdvds  13227  pockthlem  13228  pockthg  13229  pockthi  13230  prminf  13238  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  prmrec  13245  1arith  13250  4sqlem11  13278  4sqlem12  13279  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  4sqlem19  13286  prmlem1a  13384  pgpfi1  15184  pgp0  15185  sylow1lem1  15187  sylow1lem3  15189  sylow1lem4  15190  sylow1lem5  15191  odcau  15193  pgpfi  15194  fislw  15214  sylow3lem6  15221  gexexlem  15422  prmcyg  15458  ablfac1lem  15581  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem3a  15589  pgpfac1lem3  15590  ablfaclem3  15600  prmirredlem  16728  dfprm2  16729  prmirred  16730  znfld  16796  wilthlem1  20804  wilthlem2  20805  wilthlem3  20806  prmdvdsfi  20843  chtf  20844  efchtcl  20847  vmaval  20849  isppw2  20851  vmappw  20852  vmaprm  20853  vmacl  20854  vmaf  20855  efvmacl  20856  muval1  20869  chtprm  20889  chtdif  20894  efchtdvds  20895  mumul  20917  sqff1o  20918  dvdsppwf1o  20924  sgmppw  20934  0sgmppw  20935  1sgmprm  20936  vmalelog  20942  chtleppi  20947  chtublem  20948  fsumvma2  20951  vmasum  20953  chpchtsum  20956  chpub  20957  mersenne  20964  perfect1  20965  perfect  20968  pcbcctr  21013  bpos1lem  21019  bposlem1  21021  bposlem2  21022  bposlem6  21026  lgslem1  21033  lgsval2lem  21043  lgsvalmod  21052  lgsmod  21058  lgsdirprm  21066  lgsne0  21070  lgsqrlem1  21078  lgsqrlem2  21079  lgsqrlem4  21081  lgsqr  21083  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem2  21096  lgsquad2  21097  m1lgs  21099  2sqlem3  21103  2sqlem8  21109  2sqlem11  21112  2sqblem  21114  chtppilimlem1  21120  rplogsumlem2  21132  rpvmasumlem  21134  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dirith2  21175  padicabvf  21278  ostth1  21280  ostth3  21285  nn0prpwlem  26215  nn0prpw  26216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-prm 13035
  Copyright terms: Public domain W3C validator