Theorem prmnn 15388

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.

Step	Hyp	Ref	Expression
1		isprm 15387	. 2 |- ( P e. Prime <-> ( P e. NN /\ { z e. NN | z || P } ~~ 2o ) )
2	1	simplbi 476	1 |- ( P e. Prime -> P e. NN )

Syntax hints:   -> wi 4   e. wcel 1990   {crab 2916   class class class wbr 4653   2oc2o 7554   ~~ cen 7952   NNcn 11020   || cdvds 14983   Primecprime 15385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-prm 15386

This theorem is referenced by:  prmz  15389  prmssnn  15390  nprmdvds1  15418  isprm5  15419  coprm  15423  prmdvdsexpr  15429  prmndvdsfaclt  15435  cncongrprm  15437  phiprmpw  15481  fermltl  15489  prmdiv  15490  prmdiveq  15491  prmdivdiv  15492  modprm1div  15502  m1dvdsndvds  15503  vfermltl  15506  vfermltlALT  15507  powm2modprm  15508  reumodprminv  15509  modprm0  15510  nnnn0modprm0  15511  modprmn0modprm0  15512  oddprm  15515  nnoddn2prm  15516  prm23lt5  15519  pcpremul  15548  pcdvdsb  15573  pcelnn  15574  pcidlem  15576  pcid  15577  pcdvdstr  15580  pcgcd1  15581  pcprmpw2  15586  dvdsprmpweqnn  15589  dvdsprmpweqle  15590  pcaddlem  15592  pcadd  15593  pcmptcl  15595  pcmpt  15596  pcmpt2  15597  pcfaclem  15602  pcfac  15603  pcbc  15604  expnprm  15606  oddprmdvds  15607  prmpwdvds  15608  pockthlem  15609  pockthg  15610  pockthi  15611  prminf  15619  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  prmrec  15626  1arith  15631  4sqlem11  15659  4sqlem12  15660  4sqlem13  15661  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  4sqlem19  15667  prmdvdsprmo  15746  prmgaplem3  15757  prmgaplem4  15758  prmgaplem5  15759  prmgaplem6  15760  prmgaplem8  15762  cshwshashnsame  15810  cshwshash  15811  prmlem1a  15813  pgpfi1  18010  pgp0  18011  sylow1lem1  18013  sylow1lem3  18015  sylow1lem4  18016  sylow1lem5  18017  odcau  18019  pgpfi  18020  fislw  18040  sylow3lem6  18047  gexexlem  18255  prmcyg  18295  ablfac1lem  18467  ablfac1b  18469  ablfac1eu  18472  pgpfac1lem3a  18475  pgpfac1lem3  18476  ablfaclem3  18486  prmirredlem  19841  dfprm2  19842  prmirred  19843  znfld  19909  wilthlem1  24794  wilthlem2  24795  wilthlem3  24796  prmdvdsfi  24833  chtf  24834  efchtcl  24837  vmaval  24839  isppw2  24841  vmappw  24842  vmaprm  24843  vmacl  24844  efvmacl  24846  muval1  24859  chtprm  24879  chtdif  24884  efchtdvds  24885  mumul  24907  sqff1o  24908  dvdsppwf1o  24912  sgmppw  24922  0sgmppw  24923  1sgmprm  24924  vmalelog  24930  chtleppi  24935  chtublem  24936  fsumvma2  24939  vmasum  24941  chpchtsum  24944  chpub  24945  mersenne  24952  perfect1  24953  perfect  24956  pcbcctr  25001  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem6  25014  lgslem1  25022  lgsval2lem  25032  lgsvalmod  25041  lgsmod  25048  lgsdirprm  25056  lgsne0  25060  lgsprme0  25064  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem4  25074  lgsqr  25076  lgsqrmod  25077  lgsqrmodndvds  25078  gausslemma2dlem0c  25083  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  gausslemma2dlem5a  25095  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem2  25110  lgsquad2  25111  m1lgs  25113  2lgslem1a  25116  2lgslem1c  25118  2lgs  25132  2sqlem3  25145  2sqlem8  25151  2sqlem11  25154  2sqblem  25156  chtppilimlem1  25162  rplogsumlem2  25174  rpvmasumlem  25176  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dirith2  25217  padicabvf  25320  ostth1  25322  ostth3  25327  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  fusgrhashclwwlkn  26956  clwlksfclwwlk  26962  clwlksfoclwwlk  26963  clwlksf1clwwlk  26969  numclwwlk5  27246  numclwwlk6  27248  numclwwlk7  27249  numclwwlk8  27250  2sqmod  29648  nn0prpwlem  32317  nn0prpw  32318  nzprmdif  38518  etransclem41  40492  etransclem44  40495  etransclem47  40498  etransclem48  40499  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnoprmfac2  41479  prmdvdsfmtnof1lem2  41497  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  lighneal  41528  perfectALTV  41632  gbepos  41646  gbowpos  41647  sbgoldbaltlem1  41667  ztprmneprm  42125