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

Theorem prmnn 13083
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 13082 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 448 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   {crab 2710   class class class wbr 4213   2oc2o 6719    ~~ cen 7107   NNcn 10001    || cdivides 12853   Primecprime 13080
This theorem is referenced by:  prmz  13084  coprm  13101  nprmdvds1  13112  isprm5  13113  prmdvdsexpr  13117  phiprmpw  13166  fermltl  13174  prmdiv  13175  prmdiveq  13176  prmdivdiv  13177  oddprm  13190  pcpremul  13218  pcdvdsb  13243  pcelnn  13244  pcidlem  13246  pcid  13247  pcdvdstr  13250  pcgcd1  13251  pcprmpw2  13256  pcaddlem  13258  pcadd  13259  pcmptcl  13261  pcmpt  13262  pcmpt2  13263  pcfaclem  13268  pcfac  13269  pcbc  13270  expnprm  13272  prmpwdvds  13273  pockthlem  13274  pockthg  13275  pockthi  13276  prminf  13284  prmreclem4  13288  prmreclem5  13289  prmreclem6  13290  prmrec  13291  1arith  13296  4sqlem11  13324  4sqlem12  13325  4sqlem13  13326  4sqlem14  13327  4sqlem17  13330  4sqlem18  13331  4sqlem19  13332  prmlem1a  13430  pgpfi1  15230  pgp0  15231  sylow1lem1  15233  sylow1lem3  15235  sylow1lem4  15236  sylow1lem5  15237  odcau  15239  pgpfi  15240  fislw  15260  sylow3lem6  15267  gexexlem  15468  prmcyg  15504  ablfac1lem  15627  ablfac1b  15629  ablfac1eu  15632  pgpfac1lem3a  15635  pgpfac1lem3  15636  ablfaclem3  15646  prmirredlem  16774  dfprm2  16775  prmirred  16776  znfld  16842  wilthlem1  20852  wilthlem2  20853  wilthlem3  20854  prmdvdsfi  20891  chtf  20892  efchtcl  20895  vmaval  20897  isppw2  20899  vmappw  20900  vmaprm  20901  vmacl  20902  vmaf  20903  efvmacl  20904  muval1  20917  chtprm  20937  chtdif  20942  efchtdvds  20943  mumul  20965  sqff1o  20966  dvdsppwf1o  20972  sgmppw  20982  0sgmppw  20983  1sgmprm  20984  vmalelog  20990  chtleppi  20995  chtublem  20996  fsumvma2  20999  vmasum  21001  chpchtsum  21004  chpub  21005  mersenne  21012  perfect1  21013  perfect  21016  pcbcctr  21061  bpos1lem  21067  bposlem1  21069  bposlem2  21070  bposlem6  21074  lgslem1  21081  lgsval2lem  21091  lgsvalmod  21100  lgsmod  21106  lgsdirprm  21114  lgsne0  21118  lgsqrlem1  21126  lgsqrlem2  21127  lgsqrlem4  21129  lgsqr  21131  lgseisenlem1  21134  lgseisenlem2  21135  lgseisenlem3  21136  lgseisenlem4  21137  lgseisen  21138  lgsquadlem1  21139  lgsquadlem2  21140  lgsquadlem3  21141  lgsquad2lem2  21144  lgsquad2  21145  m1lgs  21147  2sqlem3  21151  2sqlem8  21157  2sqlem11  21160  2sqblem  21162  chtppilimlem1  21168  rplogsumlem2  21180  rpvmasumlem  21182  dchrisum0flblem1  21203  dchrisum0flblem2  21204  dirith2  21223  padicabvf  21326  ostth1  21328  ostth3  21333  nn0prpwlem  26326  nn0prpw  26327  modprm1div  28225  reumodprminv  28228  modprm0  28229  cshwssizelem1  28281  cshwssizesame  28289  cshwssizensame  28290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-br 4214  df-prm 13081
  Copyright terms: Public domain W3C validator