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

Theorem prmnn 13070
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 13069 . 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 1725   {crab 2701   class class class wbr 4204   2oc2o 6709    ~~ cen 7097   NNcn 9989    || cdivides 12840   Primecprime 13067
This theorem is referenced by:  prmz  13071  coprm  13088  nprmdvds1  13099  isprm5  13100  prmdvdsexpr  13104  phiprmpw  13153  fermltl  13161  prmdiv  13162  prmdiveq  13163  prmdivdiv  13164  oddprm  13177  pcpremul  13205  pcdvdsb  13230  pcelnn  13231  pcidlem  13233  pcid  13234  pcdvdstr  13237  pcgcd1  13238  pcprmpw2  13243  pcaddlem  13245  pcadd  13246  pcmptcl  13248  pcmpt  13249  pcmpt2  13250  pcfaclem  13255  pcfac  13256  pcbc  13257  expnprm  13259  prmpwdvds  13260  pockthlem  13261  pockthg  13262  pockthi  13263  prminf  13271  prmreclem4  13275  prmreclem5  13276  prmreclem6  13277  prmrec  13278  1arith  13283  4sqlem11  13311  4sqlem12  13312  4sqlem13  13313  4sqlem14  13314  4sqlem17  13317  4sqlem18  13318  4sqlem19  13319  prmlem1a  13417  pgpfi1  15217  pgp0  15218  sylow1lem1  15220  sylow1lem3  15222  sylow1lem4  15223  sylow1lem5  15224  odcau  15226  pgpfi  15227  fislw  15247  sylow3lem6  15254  gexexlem  15455  prmcyg  15491  ablfac1lem  15614  ablfac1b  15616  ablfac1eu  15619  pgpfac1lem3a  15622  pgpfac1lem3  15623  ablfaclem3  15633  prmirredlem  16761  dfprm2  16762  prmirred  16763  znfld  16829  wilthlem1  20839  wilthlem2  20840  wilthlem3  20841  prmdvdsfi  20878  chtf  20879  efchtcl  20882  vmaval  20884  isppw2  20886  vmappw  20887  vmaprm  20888  vmacl  20889  vmaf  20890  efvmacl  20891  muval1  20904  chtprm  20924  chtdif  20929  efchtdvds  20930  mumul  20952  sqff1o  20953  dvdsppwf1o  20959  sgmppw  20969  0sgmppw  20970  1sgmprm  20971  vmalelog  20977  chtleppi  20982  chtublem  20983  fsumvma2  20986  vmasum  20988  chpchtsum  20991  chpub  20992  mersenne  20999  perfect1  21000  perfect  21003  pcbcctr  21048  bpos1lem  21054  bposlem1  21056  bposlem2  21057  bposlem6  21061  lgslem1  21068  lgsval2lem  21078  lgsvalmod  21087  lgsmod  21093  lgsdirprm  21101  lgsne0  21105  lgsqrlem1  21113  lgsqrlem2  21114  lgsqrlem4  21116  lgsqr  21118  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgseisenlem4  21124  lgseisen  21125  lgsquadlem1  21126  lgsquadlem2  21127  lgsquadlem3  21128  lgsquad2lem2  21131  lgsquad2  21132  m1lgs  21134  2sqlem3  21138  2sqlem8  21144  2sqlem11  21147  2sqblem  21149  chtppilimlem1  21155  rplogsumlem2  21167  rpvmasumlem  21169  dchrisum0flblem1  21190  dchrisum0flblem2  21191  dirith2  21210  padicabvf  21313  ostth1  21315  ostth3  21320  nn0prpwlem  26262  nn0prpw  26263  modprm1div  28108  reumodprminv  28111  modprm0  28112  shwrdssizelem1  28166  shwrdssizesame  28171  shwrdssizensame  28174
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-prm 13068
  Copyright terms: Public domain W3C validator