Theorem prmnn 16643

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 16642	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 496	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3389   class class class wbr 5085  2_oc2o 8399   ≈ cen 8890  ℕcn 12174   ∥ cdvds 16221  ℙcprime 16640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-prm 16641

This theorem is referenced by:  prmz  16644  prmssnn  16645  0nprm  16647  2mulprm  16662  nprmdvds1  16676  isprm5  16677  coprm  16681  prmdvdsexpr  16687  prmndvdsfaclt  16695  prmdvdsbc  16696  prmdvdsncoprmbd  16697  cncongrprm  16699  phiprmpw  16746  fermltl  16754  prmdiv  16755  prmdiveq  16756  prmdivdiv  16757  m1dvdsndvds  16769  vfermltl  16772  vfermltlALT  16773  powm2modprm  16774  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  modprmn0modprm0  16778  oddprm  16781  nnoddn2prm  16782  prm23lt5  16785  pcpremul  16814  pcdvdsb  16840  pcelnn  16841  pcidlem  16843  pcid  16844  pcdvdstr  16847  pcgcd1  16848  pcprmpw2  16853  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcaddlem  16859  pcadd  16860  pcmptcl  16862  pcmpt  16863  pcmpt2  16864  pcfaclem  16869  pcfac  16870  pcbc  16871  expnprm  16873  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  pockthi  16878  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  1arith  16898  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  4sqlem19  16934  prmdvdsprmo  17013  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem8  17029  cshwshashnsame  17074  cshwshash  17075  prmlem1a  17077  pgpfi1  19570  pgp0  19571  sylow1lem1  19573  sylow1lem3  19575  sylow1lem4  19576  sylow1lem5  19577  odcau  19579  pgpfi  19580  fislw  19600  sylow3lem6  19607  gexexlem  19827  prmcyg  19869  ablfac1lem  20045  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem3a  20053  pgpfac1lem3  20054  ablfaclem3  20064  prmgrpsimpgd  20091  prmirredlem  21452  dfprm2  21453  prmirred  21454  fermltlchr  21509  znfld  21540  freshmansdream  21554  frobrhm  21555  ply1fermltlchr  22277  rtprmirr  26724  wilthlem1  27031  wilthlem2  27032  wilthlem3  27033  chtf  27071  efchtcl  27074  isppw2  27078  vmappw  27079  vmaprm  27080  vmacl  27081  efvmacl  27083  muval1  27096  chtprm  27116  chtdif  27121  efchtdvds  27122  dvdsppwf1o  27149  sgmppw  27160  0sgmppw  27161  1sgmprm  27162  vmalelog  27168  chtleppi  27173  chtublem  27174  fsumvma2  27177  vmasum  27179  chpchtsum  27182  chpub  27183  mersenne  27190  perfect1  27191  perfect  27194  pcbcctr  27239  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem6  27252  lgslem1  27260  lgsval2lem  27270  lgsvalmod  27279  lgsmod  27286  lgsdirprm  27294  lgsne0  27298  lgsprme0  27302  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem4  27312  lgsqr  27314  lgsqrmod  27315  lgsqrmodndvds  27316  gausslemma2dlem0c  27321  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  gausslemma2dlem5a  27333  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem3  27345  lgsquad2lem2  27348  lgsquad2  27349  m1lgs  27351  2lgslem1a  27354  2lgslem1c  27356  2lgs  27370  2sqlem3  27383  2sqlem8  27389  2sqlem11  27392  2sqblem  27394  2sqmod  27399  chtppilimlem1  27436  rplogsumlem2  27448  rpvmasumlem  27450  dchrisum0flblem1  27471  dchrisum0flblem2  27472  padicabvf  27594  ostth1  27596  ostth3  27601  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  fusgrhashclwwlkn  30149  clwlksndivn  30156  numclwwlk5  30458  numclwwlk6  30460  numclwwlk7  30461  numclwwlk8  30462  znfermltl  33426  ply1fermltl  33646  cos9thpiminplylem2  33927  nn0prpwlem  36504  nn0prpw  36505  aks4d1p6  42520  aks4d1p8d1  42523  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1  42555  aks6d1c2p1  42557  aks6d1c2p2  42558  aks6d1c3  42562  aks6d1c4  42563  aks6d1c2lem4  42566  aks6d1c5lem1  42575  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c7lem1  42619  aks6d1c7  42623  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  aks5lem8  42640  aks5  42643  nzprmdif  44746  etransclem41  46703  etransclem44  46706  etransclem47  46709  etransclem48  46710  odz2prm2pw  48026  fmtnoprmfac1lem  48027  fmtnoprmfac1  48028  fmtnoprmfac2  48030  prmdvdsfmtnof1lem2  48048  2pwp1prm  48052  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem3  48070  lighneallem4  48073  lighneal  48074  perfectALTV  48199  gbepos  48234  gbowpos  48235  sbgoldbaltlem1  48255  ztprmneprm  48823