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

Theorem prmnn 14202
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 14201 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 460 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   {crab 2797   class class class wbr 4437   2oc2o 7126    ~~ cen 7515   NNcn 10543    || cdvds 13968   Primecprime 14199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-prm 14200
This theorem is referenced by:  prmz  14203  coprm  14223  nprmdvds1  14234  isprm5  14235  prmdvdsexpr  14239  phiprmpw  14288  fermltl  14296  prmdiv  14297  prmdiveq  14298  prmdivdiv  14299  modprm1div  14306  m1dvdsndvds  14307  powm2modprm  14310  reumodprminv  14311  modprm0  14312  nnnn0modprm0  14313  modprmn0modprm0  14314  oddprm  14321  pcpremul  14349  pcdvdsb  14374  pcelnn  14375  pcidlem  14377  pcid  14378  pcdvdstr  14381  pcgcd1  14382  pcprmpw2  14387  pcaddlem  14389  pcadd  14390  pcmptcl  14392  pcmpt  14393  pcmpt2  14394  pcfaclem  14399  pcfac  14400  pcbc  14401  expnprm  14403  prmpwdvds  14404  pockthlem  14405  pockthg  14406  pockthi  14407  prminf  14415  prmreclem4  14419  prmreclem5  14420  prmreclem6  14421  prmrec  14422  1arith  14427  4sqlem11  14455  4sqlem12  14456  4sqlem13  14457  4sqlem14  14458  4sqlem17  14461  4sqlem18  14462  4sqlem19  14463  cshwshashnsame  14570  cshwshash  14571  prmlem1a  14574  pgpfi1  16594  pgp0  16595  sylow1lem1  16597  sylow1lem3  16599  sylow1lem4  16600  sylow1lem5  16601  odcau  16603  pgpfi  16604  fislw  16624  sylow3lem6  16631  gexexlem  16837  prmcyg  16875  ablfac1lem  17098  ablfac1b  17100  ablfac1eu  17103  pgpfac1lem3a  17106  pgpfac1lem3  17107  ablfaclem3  17117  prmirredlem  18501  dfprm2  18502  prmirred  18503  prmirredlemOLD  18504  dfprm2OLD  18505  prmirredOLD  18506  znfld  18577  wilthlem1  23320  wilthlem2  23321  wilthlem3  23322  prmdvdsfi  23359  chtf  23360  efchtcl  23363  vmaval  23365  isppw2  23367  vmappw  23368  vmaprm  23369  vmacl  23370  efvmacl  23372  muval1  23385  chtprm  23405  chtdif  23410  efchtdvds  23411  mumul  23433  sqff1o  23434  dvdsppwf1o  23440  sgmppw  23450  0sgmppw  23451  1sgmprm  23452  vmalelog  23458  chtleppi  23463  chtublem  23464  fsumvma2  23467  vmasum  23469  chpchtsum  23472  chpub  23473  mersenne  23480  perfect1  23481  perfect  23484  pcbcctr  23529  bpos1lem  23535  bposlem1  23537  bposlem2  23538  bposlem6  23542  lgslem1  23549  lgsval2lem  23559  lgsvalmod  23568  lgsmod  23574  lgsdirprm  23582  lgsne0  23586  lgsqrlem1  23594  lgsqrlem2  23595  lgsqrlem4  23597  lgsqr  23599  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgseisenlem4  23605  lgseisen  23606  lgsquadlem1  23607  lgsquadlem2  23608  lgsquadlem3  23609  lgsquad2lem2  23612  lgsquad2  23613  m1lgs  23615  2sqlem3  23619  2sqlem8  23625  2sqlem11  23628  2sqblem  23630  chtppilimlem1  23636  rplogsumlem2  23648  rpvmasumlem  23650  dchrisum0flblem1  23671  dchrisum0flblem2  23672  dirith2  23691  padicabvf  23794  ostth1  23796  ostth3  23801  hashecclwwlkn1  24812  usghashecclwwlk  24813  hashclwwlkn  24814  clwwlkndivn  24815  clwlkfclwwlk  24822  clwlkfoclwwlk  24823  clwlkf1clwwlk  24828  numclwwlk5  25090  numclwwlk6  25091  numclwwlk7  25092  numclwwlk8  25093  2sqmod  27614  nn0prpwlem  30116  nn0prpw  30117  nzprmdif  31200  etransclem41  32012  etransclem44  32015  etransclem47  32018  etransclem48  32019  ztprmneprm  32804
  Copyright terms: Public domain W3C validator