Theorem prmnn 16694

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.

Step	Hyp	Ref	Expression
1		isprm 16693	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 497	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3420   class class class wbr 5125  2_oc2o 8483   ≈ cen 8965  ℕcn 12249   ∥ cdvds 16273  ℙcprime 16691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-prm 16692

This theorem is referenced by:  prmz  16695  prmssnn  16696  0nprm  16698  2mulprm  16713  nprmdvds1  16726  isprm5  16727  coprm  16731  prmdvdsexpr  16737  prmndvdsfaclt  16745  prmdvdsbc  16746  prmdvdsncoprmbd  16747  cncongrprm  16749  phiprmpw  16796  fermltl  16804  prmdiv  16805  prmdiveq  16806  prmdivdiv  16807  m1dvdsndvds  16819  vfermltl  16822  vfermltlALT  16823  powm2modprm  16824  reumodprminv  16825  modprm0  16826  nnnn0modprm0  16827  modprmn0modprm0  16828  oddprm  16831  nnoddn2prm  16832  prm23lt5  16835  pcpremul  16864  pcdvdsb  16890  pcelnn  16891  pcidlem  16893  pcid  16894  pcdvdstr  16897  pcgcd1  16898  pcprmpw2  16903  dvdsprmpweqnn  16906  dvdsprmpweqle  16907  pcaddlem  16909  pcadd  16910  pcmptcl  16912  pcmpt  16913  pcmpt2  16914  pcfaclem  16919  pcfac  16920  pcbc  16921  expnprm  16923  oddprmdvds  16924  prmpwdvds  16925  pockthlem  16926  pockthg  16927  pockthi  16928  prmreclem4  16940  prmreclem5  16941  prmreclem6  16942  prmrec  16943  1arith  16948  4sqlem11  16976  4sqlem12  16977  4sqlem13  16978  4sqlem14  16979  4sqlem17  16982  4sqlem18  16983  4sqlem19  16984  prmdvdsprmo  17063  prmgaplem3  17074  prmgaplem4  17075  prmgaplem5  17076  prmgaplem6  17077  prmgaplem8  17079  cshwshashnsame  17124  cshwshash  17125  prmlem1a  17127  pgpfi1  19586  pgp0  19587  sylow1lem1  19589  sylow1lem3  19591  sylow1lem4  19592  sylow1lem5  19593  odcau  19595  pgpfi  19596  fislw  19616  sylow3lem6  19623  gexexlem  19843  prmcyg  19885  ablfac1lem  20061  ablfac1b  20063  ablfac1eu  20066  pgpfac1lem3a  20069  pgpfac1lem3  20070  ablfaclem3  20080  prmgrpsimpgd  20107  prmirredlem  21450  dfprm2  21451  prmirred  21452  fermltlchr  21511  znfld  21546  freshmansdream  21560  frobrhm  21561  ply1fermltlchr  22283  rtprmirr  26758  wilthlem1  27066  wilthlem2  27067  wilthlem3  27068  chtf  27106  efchtcl  27109  isppw2  27113  vmappw  27114  vmaprm  27115  vmacl  27116  efvmacl  27118  muval1  27131  chtprm  27151  chtdif  27156  efchtdvds  27157  dvdsppwf1o  27184  sgmppw  27196  0sgmppw  27197  1sgmprm  27198  vmalelog  27204  chtleppi  27209  chtublem  27210  fsumvma2  27213  vmasum  27215  chpchtsum  27218  chpub  27219  mersenne  27226  perfect1  27227  perfect  27230  pcbcctr  27275  bpos1lem  27281  bposlem1  27283  bposlem2  27284  bposlem6  27288  lgslem1  27296  lgsval2lem  27306  lgsvalmod  27315  lgsmod  27322  lgsdirprm  27330  lgsne0  27334  lgsprme0  27338  lgsqrlem1  27345  lgsqrlem2  27346  lgsqrlem4  27348  lgsqr  27350  lgsqrmod  27351  lgsqrmodndvds  27352  gausslemma2dlem0c  27357  gausslemma2dlem0i  27363  gausslemma2dlem1a  27364  gausslemma2dlem5a  27369  gausslemma2dlem7  27372  gausslemma2d  27373  lgseisenlem1  27374  lgseisenlem2  27375  lgseisenlem3  27376  lgseisenlem4  27377  lgsquadlem1  27379  lgsquadlem3  27381  lgsquad2lem2  27384  lgsquad2  27385  m1lgs  27387  2lgslem1a  27390  2lgslem1c  27392  2lgs  27406  2sqlem3  27419  2sqlem8  27425  2sqlem11  27428  2sqblem  27430  2sqmod  27435  chtppilimlem1  27472  rplogsumlem2  27484  rpvmasumlem  27486  dchrisum0flblem1  27507  dchrisum0flblem2  27508  padicabvf  27630  ostth1  27632  ostth3  27637  hashecclwwlkn1  30043  umgrhashecclwwlk  30044  fusgrhashclwwlkn  30045  clwlksndivn  30052  numclwwlk5  30354  numclwwlk6  30356  numclwwlk7  30357  numclwwlk8  30358  znfermltl  33335  ply1fermltl  33550  nn0prpwlem  36264  nn0prpw  36265  aks4d1p6  42023  aks4d1p8d1  42026  aks4d1p8d2  42027  aks4d1p8d3  42028  aks4d1p8  42029  aks6d1c1p2  42051  aks6d1c1p3  42052  aks6d1c1  42058  aks6d1c2p1  42060  aks6d1c2p2  42061  aks6d1c3  42065  aks6d1c4  42066  aks6d1c2lem4  42069  aks6d1c5lem1  42078  aks6d1c6lem3  42114  aks6d1c6lem4  42115  aks6d1c7lem1  42122  aks6d1c7  42126  aks5lem1  42128  aks5lem2  42129  aks5lem3a  42131  aks5lem8  42143  aks5  42146  nzprmdif  44283  etransclem41  46235  etransclem44  46238  etransclem47  46241  etransclem48  46242  odz2prm2pw  47496  fmtnoprmfac1lem  47497  fmtnoprmfac1  47498  fmtnoprmfac2  47500  prmdvdsfmtnof1lem2  47518  2pwp1prm  47522  sfprmdvdsmersenne  47536  lighneallem2  47539  lighneallem3  47540  lighneallem4  47543  lighneal  47544  perfectALTV  47656  gbepos  47691  gbowpos  47692  sbgoldbaltlem1  47712  ztprmneprm  48209