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  19509  pgp0  19510  sylow1lem1  19512  sylow1lem3  19514  sylow1lem4  19515  sylow1lem5  19516  odcau  19518  pgpfi  19519  fislw  19539  sylow3lem6  19546  gexexlem  19766  prmcyg  19808  ablfac1lem  19984  ablfac1b  19986  ablfac1eu  19989  pgpfac1lem3a  19992  pgpfac1lem3  19993  ablfaclem3  20003  prmgrpsimpgd  20030  prmirredlem  21414  dfprm2  21415  prmirred  21416  fermltlchr  21471  znfld  21502  freshmansdream  21516  frobrhm  21517  ply1fermltlchr  22232  rtprmirr  26703  wilthlem1  27011  wilthlem2  27012  wilthlem3  27013  chtf  27051  efchtcl  27054  isppw2  27058  vmappw  27059  vmaprm  27060  vmacl  27061  efvmacl  27063  muval1  27076  chtprm  27096  chtdif  27101  efchtdvds  27102  dvdsppwf1o  27129  sgmppw  27141  0sgmppw  27142  1sgmprm  27143  vmalelog  27149  chtleppi  27154  chtublem  27155  fsumvma2  27158  vmasum  27160  chpchtsum  27163  chpub  27164  mersenne  27171  perfect1  27172  perfect  27175  pcbcctr  27220  bpos1lem  27226  bposlem1  27228  bposlem2  27229  bposlem6  27233  lgslem1  27241  lgsval2lem  27251  lgsvalmod  27260  lgsmod  27267  lgsdirprm  27275  lgsne0  27279  lgsprme0  27283  lgsqrlem1  27290  lgsqrlem2  27291  lgsqrlem4  27293  lgsqr  27295  lgsqrmod  27296  lgsqrmodndvds  27297  gausslemma2dlem0c  27302  gausslemma2dlem0i  27308  gausslemma2dlem1a  27309  gausslemma2dlem5a  27314  gausslemma2dlem7  27317  gausslemma2d  27318  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgsquadlem1  27324  lgsquadlem3  27326  lgsquad2lem2  27329  lgsquad2  27330  m1lgs  27332  2lgslem1a  27335  2lgslem1c  27337  2lgs  27351  2sqlem3  27364  2sqlem8  27370  2sqlem11  27373  2sqblem  27375  2sqmod  27380  chtppilimlem1  27417  rplogsumlem2  27429  rpvmasumlem  27431  dchrisum0flblem1  27452  dchrisum0flblem2  27453  padicabvf  27575  ostth1  27577  ostth3  27582  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  fusgrhashclwwlkn  30058  clwlksndivn  30065  numclwwlk5  30367  numclwwlk6  30369  numclwwlk7  30370  numclwwlk8  30371  znfermltl  33330  ply1fermltl  33546  cos9thpiminplylem2  33766  nn0prpwlem  36303  nn0prpw  36304  aks4d1p6  42062  aks4d1p8d1  42065  aks4d1p8d2  42066  aks4d1p8d3  42067  aks4d1p8  42068  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1  42097  aks6d1c2p1  42099  aks6d1c2p2  42100  aks6d1c3  42104  aks6d1c4  42105  aks6d1c2lem4  42108  aks6d1c5lem1  42117  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7  42165  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  aks5lem8  42182  aks5  42185  nzprmdif  44301  etransclem41  46266  etransclem44  46269  etransclem47  46272  etransclem48  46273  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  48328