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

Theorem prmnn 16259
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
prmnn (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Proof of Theorem prmnn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 isprm 16258 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2o))
21simplbi 501 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  {crab 3066   class class class wbr 5068  2oc2o 8217  cen 8644  cn 11855  cdvds 15843  cprime 16256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3071  df-v 3423  df-dif 3884  df-un 3886  df-nul 4253  df-if 4455  df-sn 4557  df-pr 4559  df-op 4563  df-br 5069  df-prm 16257
This theorem is referenced by:  prmz  16260  prmssnn  16261  0nprm  16263  2mulprm  16278  nprmdvds1  16291  isprm5  16292  coprm  16296  prmdvdsexpr  16302  prmndvdsfaclt  16310  prmdvdsncoprmbd  16311  cncongrprm  16313  phiprmpw  16357  fermltl  16365  prmdiv  16366  prmdiveq  16367  prmdivdiv  16368  m1dvdsndvds  16379  vfermltl  16382  vfermltlALT  16383  powm2modprm  16384  reumodprminv  16385  modprm0  16386  nnnn0modprm0  16387  modprmn0modprm0  16388  oddprm  16391  nnoddn2prm  16392  prm23lt5  16395  pcpremul  16424  pcdvdsb  16450  pcelnn  16451  pcidlem  16453  pcid  16454  pcdvdstr  16457  pcgcd1  16458  pcprmpw2  16463  dvdsprmpweqnn  16466  dvdsprmpweqle  16467  pcaddlem  16469  pcadd  16470  pcmptcl  16472  pcmpt  16473  pcmpt2  16474  pcfaclem  16479  pcfac  16480  pcbc  16481  expnprm  16483  oddprmdvds  16484  prmpwdvds  16485  pockthlem  16486  pockthg  16487  pockthi  16488  prmreclem4  16500  prmreclem5  16501  prmreclem6  16502  prmrec  16503  1arith  16508  4sqlem11  16536  4sqlem12  16537  4sqlem13  16538  4sqlem14  16539  4sqlem17  16542  4sqlem18  16543  4sqlem19  16544  prmdvdsprmo  16623  prmgaplem3  16634  prmgaplem4  16635  prmgaplem5  16636  prmgaplem6  16637  prmgaplem8  16639  cshwshashnsame  16685  cshwshash  16686  prmlem1a  16688  pgpfi1  19012  pgp0  19013  sylow1lem1  19015  sylow1lem3  19017  sylow1lem4  19018  sylow1lem5  19019  odcau  19021  pgpfi  19022  fislw  19042  sylow3lem6  19049  gexexlem  19265  prmcyg  19307  ablfac1lem  19483  ablfac1b  19485  ablfac1eu  19488  pgpfac1lem3a  19491  pgpfac1lem3  19492  ablfaclem3  19502  prmgrpsimpgd  19529  prmirredlem  20487  dfprm2  20488  prmirred  20489  znfld  20553  wilthlem1  25977  wilthlem2  25978  wilthlem3  25979  chtf  26017  efchtcl  26020  isppw2  26024  vmappw  26025  vmaprm  26026  vmacl  26027  efvmacl  26029  muval1  26042  chtprm  26062  chtdif  26067  efchtdvds  26068  dvdsppwf1o  26095  sgmppw  26105  0sgmppw  26106  1sgmprm  26107  vmalelog  26113  chtleppi  26118  chtublem  26119  fsumvma2  26122  vmasum  26124  chpchtsum  26127  chpub  26128  mersenne  26135  perfect1  26136  perfect  26139  pcbcctr  26184  bpos1lem  26190  bposlem1  26192  bposlem2  26193  bposlem6  26197  lgslem1  26205  lgsval2lem  26215  lgsvalmod  26224  lgsmod  26231  lgsdirprm  26239  lgsne0  26243  lgsprme0  26247  lgsqrlem1  26254  lgsqrlem2  26255  lgsqrlem4  26257  lgsqr  26259  lgsqrmod  26260  lgsqrmodndvds  26261  gausslemma2dlem0c  26266  gausslemma2dlem0i  26272  gausslemma2dlem1a  26273  gausslemma2dlem5a  26278  gausslemma2dlem7  26281  gausslemma2d  26282  lgseisenlem1  26283  lgseisenlem2  26284  lgseisenlem3  26285  lgseisenlem4  26286  lgsquadlem1  26288  lgsquadlem3  26290  lgsquad2lem2  26293  lgsquad2  26294  m1lgs  26296  2lgslem1a  26299  2lgslem1c  26301  2lgs  26315  2sqlem3  26328  2sqlem8  26334  2sqlem11  26337  2sqblem  26339  2sqmod  26344  chtppilimlem1  26381  rplogsumlem2  26393  rpvmasumlem  26395  dchrisum0flblem1  26416  dchrisum0flblem2  26417  padicabvf  26539  ostth1  26541  ostth3  26546  hashecclwwlkn1  28187  umgrhashecclwwlk  28188  fusgrhashclwwlkn  28189  clwlksndivn  28196  numclwwlk5  28498  numclwwlk6  28500  numclwwlk7  28501  numclwwlk8  28502  prmdvdsbc  30877  freshmansdream  31230  frobrhm  31231  znfermltl  31303  ply1fermltl  31411  nn0prpwlem  34277  nn0prpw  34278  aks4d1p6  39852  rtprmirr  40088  nzprmdif  41643  etransclem41  43522  etransclem44  43525  etransclem47  43528  etransclem48  43529  odz2prm2pw  44719  fmtnoprmfac1lem  44720  fmtnoprmfac1  44721  fmtnoprmfac2  44723  prmdvdsfmtnof1lem2  44741  2pwp1prm  44745  sfprmdvdsmersenne  44759  lighneallem2  44762  lighneallem3  44763  lighneallem4  44766  lighneal  44767  perfectALTV  44879  gbepos  44914  gbowpos  44915  sbgoldbaltlem1  44935  ztprmneprm  45387
  Copyright terms: Public domain W3C validator