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

Theorem prmnn 12969
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 12968 . 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 1715   {crab 2632   class class class wbr 4125   2oc2o 6615    ~~ cen 7003   NNcn 9893    || cdivides 12739   Primecprime 12966
This theorem is referenced by:  prmz  12970  coprm  12987  nprmdvds1  12998  isprm5  12999  prmdvdsexpr  13003  phiprmpw  13052  fermltl  13060  prmdiv  13061  prmdiveq  13062  prmdivdiv  13063  oddprm  13076  pcpremul  13104  pcdvdsb  13129  pcelnn  13130  pcidlem  13132  pcid  13133  pcdvdstr  13136  pcgcd1  13137  pcprmpw2  13142  pcaddlem  13144  pcadd  13145  pcmptcl  13147  pcmpt  13148  pcmpt2  13149  pcfaclem  13154  pcfac  13155  pcbc  13156  expnprm  13158  prmpwdvds  13159  pockthlem  13160  pockthg  13161  pockthi  13162  prminf  13170  prmreclem4  13174  prmreclem5  13175  prmreclem6  13176  prmrec  13177  1arith  13182  4sqlem11  13210  4sqlem12  13211  4sqlem13  13212  4sqlem14  13213  4sqlem17  13216  4sqlem18  13217  4sqlem19  13218  prmlem1a  13316  pgpfi1  15116  pgp0  15117  sylow1lem1  15119  sylow1lem3  15121  sylow1lem4  15122  sylow1lem5  15123  odcau  15125  pgpfi  15126  fislw  15146  sylow3lem6  15153  gexexlem  15354  prmcyg  15390  ablfac1lem  15513  ablfac1b  15515  ablfac1eu  15518  pgpfac1lem3a  15521  pgpfac1lem3  15522  ablfaclem3  15532  prmirredlem  16663  dfprm2  16664  prmirred  16665  znfld  16731  wilthlem1  20529  wilthlem2  20530  wilthlem3  20531  prmdvdsfi  20568  chtf  20569  efchtcl  20572  vmaval  20574  isppw2  20576  vmappw  20577  vmaprm  20578  vmacl  20579  vmaf  20580  efvmacl  20581  muval1  20594  chtprm  20614  chtdif  20619  efchtdvds  20620  mumul  20642  sqff1o  20643  dvdsppwf1o  20649  sgmppw  20659  0sgmppw  20660  1sgmprm  20661  vmalelog  20667  chtleppi  20672  chtublem  20673  fsumvma2  20676  vmasum  20678  chpchtsum  20681  chpub  20682  mersenne  20689  perfect1  20690  perfect  20693  pcbcctr  20738  bpos1lem  20744  bposlem1  20746  bposlem2  20747  bposlem6  20751  lgslem1  20758  lgsval2lem  20768  lgsvalmod  20777  lgsmod  20783  lgsdirprm  20791  lgsne0  20795  lgsqrlem1  20803  lgsqrlem2  20804  lgsqrlem4  20806  lgsqr  20808  lgseisenlem1  20811  lgseisenlem2  20812  lgseisenlem3  20813  lgseisenlem4  20814  lgseisen  20815  lgsquadlem1  20816  lgsquadlem2  20817  lgsquadlem3  20818  lgsquad2lem2  20821  lgsquad2  20822  m1lgs  20824  2sqlem3  20828  2sqlem8  20834  2sqlem11  20837  2sqblem  20839  chtppilimlem1  20845  rplogsumlem2  20857  rpvmasumlem  20859  dchrisum0flblem1  20880  dchrisum0flblem2  20881  dirith2  20900  padicabvf  21003  ostth1  21005  ostth3  21010  nn0prpwlem  25830  nn0prpw  25831
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-prm 12967
  Copyright terms: Public domain W3C validator