Theorem prmnn 16727

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

Syntax hints:   → wi 4   ∈ wcel 2143  {crab 3416   class class class wbr 5109  2_oc2o 8443   ≈ cen 8936  ℕcn 12228   ∥ cdvds 16305  ℙcprime 16724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-prm 16725

This theorem is referenced by:  prmz  16728  prmssnn  16729  0nprm  16731  2mulprm  16746  nprmdvds1  16760  isprm5  16761  coprm  16765  prmdvdsexpr  16771  prmndvdsfaclt  16779  prmdvdsbc  16780  prmdvdsncoprmbd  16781  cncongrprm  16783  phiprmpw  16830  fermltl  16838  prmdiv  16839  prmdiveq  16840  prmdivdiv  16841  m1dvdsndvds  16853  vfermltl  16856  vfermltlALT  16857  powm2modprm  16858  reumodprminv  16859  modprm0  16860  nnnn0modprm0  16861  modprmn0modprm0  16862  oddprm  16865  nnoddn2prm  16866  prm23lt5  16869  pcpremul  16898  pcdvdsb  16924  pcelnn  16925  pcidlem  16927  pcid  16928  pcdvdstr  16931  pcgcd1  16932  pcprmpw2  16937  dvdsprmpweqnn  16940  dvdsprmpweqle  16941  pcaddlem  16943  pcadd  16944  pcmptcl  16946  pcmpt  16947  pcmpt2  16948  pcfaclem  16953  pcfac  16954  pcbc  16955  expnprm  16957  oddprmdvds  16958  prmpwdvds  16959  pockthlem  16960  pockthg  16961  pockthi  16962  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  prmrec  16977  1arith  16982  4sqlem11  17010  4sqlem12  17011  4sqlem13  17012  4sqlem14  17013  4sqlem17  17016  4sqlem18  17017  4sqlem19  17018  prmdvdsprmo  17097  prmgaplem3  17108  prmgaplem4  17109  prmgaplem5  17110  prmgaplem6  17111  prmgaplem8  17113  cshwshashnsame  17158  cshwshash  17159  prmlem1a  17161  pgpfi1  19660  pgp0  19661  sylow1lem1  19663  sylow1lem3  19665  sylow1lem4  19666  sylow1lem5  19667  odcau  19669  pgpfi  19670  fislw  19690  sylow3lem6  19697  gexexlem  19917  prmcyg  19959  ablfac1lem  20135  ablfac1b  20137  ablfac1eu  20140  pgpfac1lem3a  20143  pgpfac1lem3  20144  ablfaclem3  20154  prmgrpsimpgd  20181  prmirredlem  21622  dfprm2  21623  prmirred  21624  fermltlchr  21679  znfld  21710  freshmansdream  21724  frobrhm  21725  ply1fermltlchr  22472  rtprmirr  26925  wilthlem1  27232  wilthlem2  27233  wilthlem3  27234  chtf  27272  efchtcl  27275  isppw2  27279  vmappw  27280  vmaprm  27281  vmacl  27282  efvmacl  27284  muval1  27297  chtprm  27317  chtdif  27322  efchtdvds  27323  dvdsppwf1o  27350  sgmppw  27361  0sgmppw  27362  1sgmprm  27363  vmalelog  27369  chtleppi  27374  chtublem  27375  fsumvma2  27378  vmasum  27380  chpchtsum  27383  chpub  27384  mersenne  27391  perfect1  27392  perfect  27395  pcbcctr  27440  bpos1lem  27446  bposlem1  27448  bposlem2  27449  bposlem6  27453  lgslem1  27461  lgsval2lem  27471  lgsvalmod  27480  lgsmod  27487  lgsdirprm  27495  lgsne0  27499  lgsprme0  27503  lgsqrlem1  27510  lgsqrlem2  27511  lgsqrlem4  27513  lgsqr  27515  lgsqrmod  27516  lgsqrmodndvds  27517  gausslemma2dlem0c  27522  gausslemma2dlem0i  27528  gausslemma2dlem1a  27529  gausslemma2dlem5a  27534  gausslemma2dlem7  27537  gausslemma2d  27538  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgsquadlem1  27544  lgsquadlem3  27546  lgsquad2lem2  27549  lgsquad2  27550  m1lgs  27552  2lgslem1a  27555  2lgslem1c  27557  2lgs  27571  2sqlem3  27584  2sqlem8  27590  2sqlem11  27593  2sqblem  27595  2sqmod  27600  chtppilimlem1  27637  rplogsumlem2  27649  rpvmasumlem  27651  dchrisum0flblem1  27672  dchrisum0flblem2  27673  padicabvf  27795  ostth1  27797  ostth3  27802  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  fusgrhashclwwlkn  30430  clwlksndivn  30437  numclwwlk5  30739  numclwwlk6  30741  numclwwlk7  30742  numclwwlk8  30743  znfermltl  33681  ply1fermltl  33876  cos9thpiminplylem2  34173  nn0prpwlem  36833  nn0prpw  36834  aks4d1p6  42848  aks4d1p8d1  42851  aks4d1p8d2  42852  aks4d1p8d3  42853  aks4d1p8  42854  aks6d1c1p2  42876  aks6d1c1p3  42877  aks6d1c1  42883  aks6d1c2p1  42885  aks6d1c2p2  42886  aks6d1c3  42890  aks6d1c4  42891  aks6d1c2lem4  42894  aks6d1c5lem1  42903  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c7lem1  42947  aks6d1c7  42951  aks5lem1  42953  aks5lem2  42954  aks5lem3a  42956  aks5lem8  42968  aks5  42971  nzprmdif  45029  etransclem41  46989  etransclem44  46992  etransclem47  46995  etransclem48  46996  odz2prm2pw  48315  fmtnoprmfac1lem  48316  fmtnoprmfac1  48317  fmtnoprmfac2  48319  prmdvdsfmtnof1lem2  48337  2pwp1prm  48341  sfprmdvdsmersenne  48355  lighneallem2  48358  lighneallem3  48359  lighneallem4  48362  lighneal  48363  perfectALTV  48488  gbepos  48523  gbowpos  48524  sbgoldbaltlem1  48544  ztprmneprm  49127