Theorem prmnn 16601

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3399   class class class wbr 5098  2_oc2o 8391   ≈ cen 8880  ℕcn 12145   ∥ cdvds 16179  ℙcprime 16598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-prm 16599

This theorem is referenced by:  prmz  16602  prmssnn  16603  0nprm  16605  2mulprm  16620  nprmdvds1  16633  isprm5  16634  coprm  16638  prmdvdsexpr  16644  prmndvdsfaclt  16652  prmdvdsbc  16653  prmdvdsncoprmbd  16654  cncongrprm  16656  phiprmpw  16703  fermltl  16711  prmdiv  16712  prmdiveq  16713  prmdivdiv  16714  m1dvdsndvds  16726  vfermltl  16729  vfermltlALT  16730  powm2modprm  16731  reumodprminv  16732  modprm0  16733  nnnn0modprm0  16734  modprmn0modprm0  16735  oddprm  16738  nnoddn2prm  16739  prm23lt5  16742  pcpremul  16771  pcdvdsb  16797  pcelnn  16798  pcidlem  16800  pcid  16801  pcdvdstr  16804  pcgcd1  16805  pcprmpw2  16810  dvdsprmpweqnn  16813  dvdsprmpweqle  16814  pcaddlem  16816  pcadd  16817  pcmptcl  16819  pcmpt  16820  pcmpt2  16821  pcfaclem  16826  pcfac  16827  pcbc  16828  expnprm  16830  oddprmdvds  16831  prmpwdvds  16832  pockthlem  16833  pockthg  16834  pockthi  16835  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  prmrec  16850  1arith  16855  4sqlem11  16883  4sqlem12  16884  4sqlem13  16885  4sqlem14  16886  4sqlem17  16889  4sqlem18  16890  4sqlem19  16891  prmdvdsprmo  16970  prmgaplem3  16981  prmgaplem4  16982  prmgaplem5  16983  prmgaplem6  16984  prmgaplem8  16986  cshwshashnsame  17031  cshwshash  17032  prmlem1a  17034  pgpfi1  19524  pgp0  19525  sylow1lem1  19527  sylow1lem3  19529  sylow1lem4  19530  sylow1lem5  19531  odcau  19533  pgpfi  19534  fislw  19554  sylow3lem6  19561  gexexlem  19781  prmcyg  19823  ablfac1lem  19999  ablfac1b  20001  ablfac1eu  20004  pgpfac1lem3a  20007  pgpfac1lem3  20008  ablfaclem3  20018  prmgrpsimpgd  20045  prmirredlem  21427  dfprm2  21428  prmirred  21429  fermltlchr  21484  znfld  21515  freshmansdream  21529  frobrhm  21530  ply1fermltlchr  22256  rtprmirr  26726  wilthlem1  27034  wilthlem2  27035  wilthlem3  27036  chtf  27074  efchtcl  27077  isppw2  27081  vmappw  27082  vmaprm  27083  vmacl  27084  efvmacl  27086  muval1  27099  chtprm  27119  chtdif  27124  efchtdvds  27125  dvdsppwf1o  27152  sgmppw  27164  0sgmppw  27165  1sgmprm  27166  vmalelog  27172  chtleppi  27177  chtublem  27178  fsumvma2  27181  vmasum  27183  chpchtsum  27186  chpub  27187  mersenne  27194  perfect1  27195  perfect  27198  pcbcctr  27243  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem6  27256  lgslem1  27264  lgsval2lem  27274  lgsvalmod  27283  lgsmod  27290  lgsdirprm  27298  lgsne0  27302  lgsprme0  27306  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem4  27316  lgsqr  27318  lgsqrmod  27319  lgsqrmodndvds  27320  gausslemma2dlem0c  27325  gausslemma2dlem0i  27331  gausslemma2dlem1a  27332  gausslemma2dlem5a  27337  gausslemma2dlem7  27340  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem3  27349  lgsquad2lem2  27352  lgsquad2  27353  m1lgs  27355  2lgslem1a  27358  2lgslem1c  27360  2lgs  27374  2sqlem3  27387  2sqlem8  27393  2sqlem11  27396  2sqblem  27398  2sqmod  27403  chtppilimlem1  27440  rplogsumlem2  27452  rpvmasumlem  27454  dchrisum0flblem1  27475  dchrisum0flblem2  27476  padicabvf  27598  ostth1  27600  ostth3  27605  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  fusgrhashclwwlkn  30154  clwlksndivn  30161  numclwwlk5  30463  numclwwlk6  30465  numclwwlk7  30466  numclwwlk8  30467  znfermltl  33447  ply1fermltl  33667  cos9thpiminplylem2  33940  nn0prpwlem  36516  nn0prpw  36517  aks4d1p6  42335  aks4d1p8d1  42338  aks4d1p8d2  42339  aks4d1p8d3  42340  aks4d1p8  42341  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1  42370  aks6d1c2p1  42372  aks6d1c2p2  42373  aks6d1c3  42377  aks6d1c4  42378  aks6d1c2lem4  42381  aks6d1c5lem1  42390  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c7lem1  42434  aks6d1c7  42438  aks5lem1  42440  aks5lem2  42441  aks5lem3a  42443  aks5lem8  42455  aks5  42458  nzprmdif  44560  etransclem41  46519  etransclem44  46522  etransclem47  46525  etransclem48  46526  odz2prm2pw  47809  fmtnoprmfac1lem  47810  fmtnoprmfac1  47811  fmtnoprmfac2  47813  prmdvdsfmtnof1lem2  47831  2pwp1prm  47835  sfprmdvdsmersenne  47849  lighneallem2  47852  lighneallem3  47853  lighneallem4  47856  lighneal  47857  perfectALTV  47969  gbepos  48004  gbowpos  48005  sbgoldbaltlem1  48025  ztprmneprm  48593