Theorem prmnn 16698

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3420   class class class wbr 5124  2_oc2o 8479   ≈ cen 8961  ℕcn 12245   ∥ cdvds 16277  ℙcprime 16695

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-prm 16696

This theorem is referenced by:  prmz  16699  prmssnn  16700  0nprm  16702  2mulprm  16717  nprmdvds1  16730  isprm5  16731  coprm  16735  prmdvdsexpr  16741  prmndvdsfaclt  16749  prmdvdsbc  16750  prmdvdsncoprmbd  16751  cncongrprm  16753  phiprmpw  16800  fermltl  16808  prmdiv  16809  prmdiveq  16810  prmdivdiv  16811  m1dvdsndvds  16823  vfermltl  16826  vfermltlALT  16827  powm2modprm  16828  reumodprminv  16829  modprm0  16830  nnnn0modprm0  16831  modprmn0modprm0  16832  oddprm  16835  nnoddn2prm  16836  prm23lt5  16839  pcpremul  16868  pcdvdsb  16894  pcelnn  16895  pcidlem  16897  pcid  16898  pcdvdstr  16901  pcgcd1  16902  pcprmpw2  16907  dvdsprmpweqnn  16910  dvdsprmpweqle  16911  pcaddlem  16913  pcadd  16914  pcmptcl  16916  pcmpt  16917  pcmpt2  16918  pcfaclem  16923  pcfac  16924  pcbc  16925  expnprm  16927  oddprmdvds  16928  prmpwdvds  16929  pockthlem  16930  pockthg  16931  pockthi  16932  prmreclem4  16944  prmreclem5  16945  prmreclem6  16946  prmrec  16947  1arith  16952  4sqlem11  16980  4sqlem12  16981  4sqlem13  16982  4sqlem14  16983  4sqlem17  16986  4sqlem18  16987  4sqlem19  16988  prmdvdsprmo  17067  prmgaplem3  17078  prmgaplem4  17079  prmgaplem5  17080  prmgaplem6  17081  prmgaplem8  17083  cshwshashnsame  17128  cshwshash  17129  prmlem1a  17131  pgpfi1  19581  pgp0  19582  sylow1lem1  19584  sylow1lem3  19586  sylow1lem4  19587  sylow1lem5  19588  odcau  19590  pgpfi  19591  fislw  19611  sylow3lem6  19618  gexexlem  19838  prmcyg  19880  ablfac1lem  20056  ablfac1b  20058  ablfac1eu  20061  pgpfac1lem3a  20064  pgpfac1lem3  20065  ablfaclem3  20075  prmgrpsimpgd  20102  prmirredlem  21438  dfprm2  21439  prmirred  21440  fermltlchr  21495  znfld  21526  freshmansdream  21540  frobrhm  21541  ply1fermltlchr  22255  rtprmirr  26727  wilthlem1  27035  wilthlem2  27036  wilthlem3  27037  chtf  27075  efchtcl  27078  isppw2  27082  vmappw  27083  vmaprm  27084  vmacl  27085  efvmacl  27087  muval1  27100  chtprm  27120  chtdif  27125  efchtdvds  27126  dvdsppwf1o  27153  sgmppw  27165  0sgmppw  27166  1sgmprm  27167  vmalelog  27173  chtleppi  27178  chtublem  27179  fsumvma2  27182  vmasum  27184  chpchtsum  27187  chpub  27188  mersenne  27195  perfect1  27196  perfect  27199  pcbcctr  27244  bpos1lem  27250  bposlem1  27252  bposlem2  27253  bposlem6  27257  lgslem1  27265  lgsval2lem  27275  lgsvalmod  27284  lgsmod  27291  lgsdirprm  27299  lgsne0  27303  lgsprme0  27307  lgsqrlem1  27314  lgsqrlem2  27315  lgsqrlem4  27317  lgsqr  27319  lgsqrmod  27320  lgsqrmodndvds  27321  gausslemma2dlem0c  27326  gausslemma2dlem0i  27332  gausslemma2dlem1a  27333  gausslemma2dlem5a  27338  gausslemma2dlem7  27341  gausslemma2d  27342  lgseisenlem1  27343  lgseisenlem2  27344  lgseisenlem3  27345  lgseisenlem4  27346  lgsquadlem1  27348  lgsquadlem3  27350  lgsquad2lem2  27353  lgsquad2  27354  m1lgs  27356  2lgslem1a  27359  2lgslem1c  27361  2lgs  27375  2sqlem3  27388  2sqlem8  27394  2sqlem11  27397  2sqblem  27399  2sqmod  27404  chtppilimlem1  27441  rplogsumlem2  27453  rpvmasumlem  27455  dchrisum0flblem1  27476  dchrisum0flblem2  27477  padicabvf  27599  ostth1  27601  ostth3  27606  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  fusgrhashclwwlkn  30065  clwlksndivn  30072  numclwwlk5  30374  numclwwlk6  30376  numclwwlk7  30377  numclwwlk8  30378  znfermltl  33386  ply1fermltl  33602  cos9thpiminplylem2  33822  nn0prpwlem  36345  nn0prpw  36346  aks4d1p6  42099  aks4d1p8d1  42102  aks4d1p8d2  42103  aks4d1p8d3  42104  aks4d1p8  42105  aks6d1c1p2  42127  aks6d1c1p3  42128  aks6d1c1  42134  aks6d1c2p1  42136  aks6d1c2p2  42137  aks6d1c3  42141  aks6d1c4  42142  aks6d1c2lem4  42145  aks6d1c5lem1  42154  aks6d1c6lem3  42190  aks6d1c6lem4  42191  aks6d1c7lem1  42198  aks6d1c7  42202  aks5lem1  42204  aks5lem2  42205  aks5lem3a  42207  aks5lem8  42219  aks5  42222  nzprmdif  44318  etransclem41  46284  etransclem44  46287  etransclem47  46290  etransclem48  46291  odz2prm2pw  47557  fmtnoprmfac1lem  47558  fmtnoprmfac1  47559  fmtnoprmfac2  47561  prmdvdsfmtnof1lem2  47579  2pwp1prm  47583  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem3  47601  lighneallem4  47604  lighneal  47605  perfectALTV  47717  gbepos  47752  gbowpos  47753  sbgoldbaltlem1  47773  ztprmneprm  48302