Theorem prmnn 16620

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3402   class class class wbr 5102  2_oc2o 8405   ≈ cen 8892  ℕcn 12162   ∥ cdvds 16198  ℙcprime 16617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-prm 16618

This theorem is referenced by:  prmz  16621  prmssnn  16622  0nprm  16624  2mulprm  16639  nprmdvds1  16652  isprm5  16653  coprm  16657  prmdvdsexpr  16663  prmndvdsfaclt  16671  prmdvdsbc  16672  prmdvdsncoprmbd  16673  cncongrprm  16675  phiprmpw  16722  fermltl  16730  prmdiv  16731  prmdiveq  16732  prmdivdiv  16733  m1dvdsndvds  16745  vfermltl  16748  vfermltlALT  16749  powm2modprm  16750  reumodprminv  16751  modprm0  16752  nnnn0modprm0  16753  modprmn0modprm0  16754  oddprm  16757  nnoddn2prm  16758  prm23lt5  16761  pcpremul  16790  pcdvdsb  16816  pcelnn  16817  pcidlem  16819  pcid  16820  pcdvdstr  16823  pcgcd1  16824  pcprmpw2  16829  dvdsprmpweqnn  16832  dvdsprmpweqle  16833  pcaddlem  16835  pcadd  16836  pcmptcl  16838  pcmpt  16839  pcmpt2  16840  pcfaclem  16845  pcfac  16846  pcbc  16847  expnprm  16849  oddprmdvds  16850  prmpwdvds  16851  pockthlem  16852  pockthg  16853  pockthi  16854  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  prmrec  16869  1arith  16874  4sqlem11  16902  4sqlem12  16903  4sqlem13  16904  4sqlem14  16905  4sqlem17  16908  4sqlem18  16909  4sqlem19  16910  prmdvdsprmo  16989  prmgaplem3  17000  prmgaplem4  17001  prmgaplem5  17002  prmgaplem6  17003  prmgaplem8  17005  cshwshashnsame  17050  cshwshash  17051  prmlem1a  17053  pgpfi1  19501  pgp0  19502  sylow1lem1  19504  sylow1lem3  19506  sylow1lem4  19507  sylow1lem5  19508  odcau  19510  pgpfi  19511  fislw  19531  sylow3lem6  19538  gexexlem  19758  prmcyg  19800  ablfac1lem  19976  ablfac1b  19978  ablfac1eu  19981  pgpfac1lem3a  19984  pgpfac1lem3  19985  ablfaclem3  19995  prmgrpsimpgd  20022  prmirredlem  21358  dfprm2  21359  prmirred  21360  fermltlchr  21415  znfld  21446  freshmansdream  21460  frobrhm  21461  ply1fermltlchr  22175  rtprmirr  26646  wilthlem1  26954  wilthlem2  26955  wilthlem3  26956  chtf  26994  efchtcl  26997  isppw2  27001  vmappw  27002  vmaprm  27003  vmacl  27004  efvmacl  27006  muval1  27019  chtprm  27039  chtdif  27044  efchtdvds  27045  dvdsppwf1o  27072  sgmppw  27084  0sgmppw  27085  1sgmprm  27086  vmalelog  27092  chtleppi  27097  chtublem  27098  fsumvma2  27101  vmasum  27103  chpchtsum  27106  chpub  27107  mersenne  27114  perfect1  27115  perfect  27118  pcbcctr  27163  bpos1lem  27169  bposlem1  27171  bposlem2  27172  bposlem6  27176  lgslem1  27184  lgsval2lem  27194  lgsvalmod  27203  lgsmod  27210  lgsdirprm  27218  lgsne0  27222  lgsprme0  27226  lgsqrlem1  27233  lgsqrlem2  27234  lgsqrlem4  27236  lgsqr  27238  lgsqrmod  27239  lgsqrmodndvds  27240  gausslemma2dlem0c  27245  gausslemma2dlem0i  27251  gausslemma2dlem1a  27252  gausslemma2dlem5a  27257  gausslemma2dlem7  27260  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  lgsquadlem3  27269  lgsquad2lem2  27272  lgsquad2  27273  m1lgs  27275  2lgslem1a  27278  2lgslem1c  27280  2lgs  27294  2sqlem3  27307  2sqlem8  27313  2sqlem11  27316  2sqblem  27318  2sqmod  27323  chtppilimlem1  27360  rplogsumlem2  27372  rpvmasumlem  27374  dchrisum0flblem1  27395  dchrisum0flblem2  27396  padicabvf  27518  ostth1  27520  ostth3  27525  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  fusgrhashclwwlkn  29981  clwlksndivn  29988  numclwwlk5  30290  numclwwlk6  30292  numclwwlk7  30293  numclwwlk8  30294  znfermltl  33310  ply1fermltl  33526  cos9thpiminplylem2  33746  nn0prpwlem  36283  nn0prpw  36284  aks4d1p6  42042  aks4d1p8d1  42045  aks4d1p8d2  42046  aks4d1p8d3  42047  aks4d1p8  42048  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1  42077  aks6d1c2p1  42079  aks6d1c2p2  42080  aks6d1c3  42084  aks6d1c4  42085  aks6d1c2lem4  42088  aks6d1c5lem1  42097  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c7lem1  42141  aks6d1c7  42145  aks5lem1  42147  aks5lem2  42148  aks5lem3a  42150  aks5lem8  42162  aks5  42165  nzprmdif  44281  etransclem41  46246  etransclem44  46249  etransclem47  46252  etransclem48  46253  odz2prm2pw  47537  fmtnoprmfac1lem  47538  fmtnoprmfac1  47539  fmtnoprmfac2  47541  prmdvdsfmtnof1lem2  47559  2pwp1prm  47563  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem3  47581  lighneallem4  47584  lighneal  47585  perfectALTV  47697  gbepos  47732  gbowpos  47733  sbgoldbaltlem1  47753  ztprmneprm  48308