Theorem prmnn 16858

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  {crab 3412   class class class wbr 5102  2_oc2o 8477   ≈ cen 8977  ℕcn 12342   ∥ cdvds 16431  ℙcprime 16855

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-prm 16856

This theorem is used by:  prmz  16859  prmssnn  16860  0nprm  16862  2mulprm  16877  nprmdvds1  16891  isprm5  16892  coprm  16896  prmdvdsexpr  16902  prmndvdsfaclt  16910  prmdvdsbc  16911  prmdvdsncoprmbd  16912  cncongrprm  16914  phiprmpw  16962  fermltl  16970  prmdiv  16971  prmdiveq  16972  prmdivdiv  16973  m1dvdsndvds  16985  vfermltl  16988  vfermltlALT  16989  powm2modprm  16990  reumodprminv  16991  modprm0  16992  nnnn0modprm0  16993  modprmn0modprm0  16994  oddprm  16997  nnoddn2prm  16998  prm23lt5  17001  pcpremul  17030  pcdvdsb  17056  pcelnn  17057  pcidlem  17059  pcid  17060  pcdvdstr  17063  pcgcd1  17064  pcprmpw2  17069  dvdsprmpweqnn  17072  dvdsprmpweqle  17073  pcaddlem  17075  pcadd  17076  pcmptcl  17078  pcmpt  17079  pcmpt2  17080  pcfaclem  17085  pcfac  17086  pcbc  17087  expnprm  17089  oddprmdvds  17090  prmpwdvds  17091  pockthlem  17092  pockthg  17093  pockthi  17094  prmreclem4  17106  prmreclem5  17107  prmreclem6  17108  prmrec  17109  1arith  17114  4sqlem11  17142  4sqlem12  17143  4sqlem13  17144  4sqlem14  17145  4sqlem17  17148  4sqlem18  17149  4sqlem19  17150  prmdvdsprmo  17229  prmgaplem3  17240  prmgaplem4  17241  prmgaplem5  17242  prmgaplem6  17243  prmgaplem8  17245  cshwshashnsame  17290  cshwshash  17291  prmlem1a  17293  pgpfi1  19818  pgp0  19819  sylow1lem1  19821  sylow1lem3  19823  sylow1lem4  19824  sylow1lem5  19825  odcau  19827  pgpfi  19828  fislw  19848  sylow3lem6  19855  gexexlem  20075  prmcyg  20117  ablfac1lem  20293  ablfac1b  20295  ablfac1eu  20298  pgpfac1lem3a  20301  pgpfac1lem3  20302  ablfaclem3  20312  prmgrpsimpgd  20339  prmirredlem  21787  dfprm2  21788  prmirred  21789  fermltlchr  21844  znfld  21875  freshmansdream  21889  frobrhm  21890  ply1fermltlchr  22639  rtprmirr  27097  wilthlem1  27404  wilthlem2  27405  wilthlem3  27406  chtf  27444  efchtcl  27447  isppw2  27451  vmappw  27452  vmaprm  27453  vmacl  27454  efvmacl  27456  muval1  27469  chtprm  27489  chtdif  27494  efchtdvds  27495  dvdsppwf1o  27522  sgmppw  27533  0sgmppw  27534  1sgmprm  27535  vmalelog  27541  chtleppi  27546  chtublem  27547  fsumvma2  27550  vmasum  27552  chpchtsum  27555  chpub  27556  mersenne  27563  perfect1  27564  perfect  27567  pcbcctr  27612  bpos1lem  27618  bposlem1  27620  bposlem2  27621  bposlem6  27625  lgslem1  27633  lgsval2lem  27643  lgsvalmod  27652  lgsmod  27659  lgsdirprm  27667  lgsne0  27671  lgsprme0  27675  lgsqrlem1  27682  lgsqrlem2  27683  lgsqrlem4  27685  lgsqr  27687  lgsqrmod  27688  lgsqrmodndvds  27689  gausslemma2dlem0c  27694  gausslemma2dlem0i  27700  gausslemma2dlem1a  27701  gausslemma2dlem5a  27706  gausslemma2dlem7  27709  gausslemma2d  27710  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisenlem4  27714  lgsquadlem1  27716  lgsquadlem3  27718  lgsquad2lem2  27721  lgsquad2  27722  m1lgs  27724  2lgslem1a  27727  2lgslem1c  27729  2lgs  27743  2sqlem3  27756  2sqlem8  27762  2sqlem11  27765  2sqblem  27767  2sqmod  27772  chtppilimlem1  27809  rplogsumlem2  27821  rpvmasumlem  27823  dchrisum0flblem1  27844  dchrisum0flblem2  27845  padicabvf  27967  ostth1  27969  ostth3  27974  fltoprm  28004  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  fusgrhashclwwlkn  30679  clwlksndivn  30686  numclwwlk5  30998  numclwwlk6  31000  numclwwlk7  31001  numclwwlk8  31002  znfermltl  33972  ply1fermltl  34168  cos9thpiminplylem2  34465  nn0prpwlem  37206  nn0prpw  37207  aks4d1p6  43240  aks4d1p8d1  43243  aks4d1p8d2  43244  aks4d1p8d3  43245  aks4d1p8  43246  aks6d1c1p2  43268  aks6d1c1p3  43269  aks6d1c1  43275  aks6d1c2p1  43277  aks6d1c2p2  43278  aks6d1c3  43282  aks6d1c4  43283  aks6d1c2lem4  43286  aks6d1c5lem1  43295  aks6d1c6lem3  43331  aks6d1c6lem4  43332  aks6d1c7lem1  43339  aks6d1c7  43343  aks5lem1  43345  aks5lem2  43346  aks5lem3a  43348  aks5lem8  43360  aks5  43363  nzprmdif  45412  etransclem41  47393  etransclem44  47396  etransclem47  47399  etransclem48  47400  odz2prm2pw  48756  fmtnoprmfac1lem  48757  fmtnoprmfac1  48758  fmtnoprmfac2  48760  prmdvdsfmtnof1lem2  48778  2pwp1prm  48782  sfprmdvdsmersenne  48796  lighneallem2  48799  lighneallem3  48800  lighneallem4  48803  lighneal  48804  perfectALTV  48929  gbepos  48964  gbowpos  48965  sbgoldbaltlem1  48985  ztprmneprm  49567