Theorem prmnn 16708

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

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3433   class class class wbr 5148  2_oc2o 8499   ≈ cen 8981  ℕcn 12264   ∥ cdvds 16287  ℙcprime 16705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-prm 16706

This theorem is referenced by:  prmz  16709  prmssnn  16710  0nprm  16712  2mulprm  16727  nprmdvds1  16740  isprm5  16741  coprm  16745  prmdvdsexpr  16751  prmndvdsfaclt  16759  prmdvdsbc  16760  prmdvdsncoprmbd  16761  cncongrprm  16763  phiprmpw  16810  fermltl  16818  prmdiv  16819  prmdiveq  16820  prmdivdiv  16821  m1dvdsndvds  16832  vfermltl  16835  vfermltlALT  16836  powm2modprm  16837  reumodprminv  16838  modprm0  16839  nnnn0modprm0  16840  modprmn0modprm0  16841  oddprm  16844  nnoddn2prm  16845  prm23lt5  16848  pcpremul  16877  pcdvdsb  16903  pcelnn  16904  pcidlem  16906  pcid  16907  pcdvdstr  16910  pcgcd1  16911  pcprmpw2  16916  dvdsprmpweqnn  16919  dvdsprmpweqle  16920  pcaddlem  16922  pcadd  16923  pcmptcl  16925  pcmpt  16926  pcmpt2  16927  pcfaclem  16932  pcfac  16933  pcbc  16934  expnprm  16936  oddprmdvds  16937  prmpwdvds  16938  pockthlem  16939  pockthg  16940  pockthi  16941  prmreclem4  16953  prmreclem5  16954  prmreclem6  16955  prmrec  16956  1arith  16961  4sqlem11  16989  4sqlem12  16990  4sqlem13  16991  4sqlem14  16992  4sqlem17  16995  4sqlem18  16996  4sqlem19  16997  prmdvdsprmo  17076  prmgaplem3  17087  prmgaplem4  17088  prmgaplem5  17089  prmgaplem6  17090  prmgaplem8  17092  cshwshashnsame  17138  cshwshash  17139  prmlem1a  17141  pgpfi1  19628  pgp0  19629  sylow1lem1  19631  sylow1lem3  19633  sylow1lem4  19634  sylow1lem5  19635  odcau  19637  pgpfi  19638  fislw  19658  sylow3lem6  19665  gexexlem  19885  prmcyg  19927  ablfac1lem  20103  ablfac1b  20105  ablfac1eu  20108  pgpfac1lem3a  20111  pgpfac1lem3  20112  ablfaclem3  20122  prmgrpsimpgd  20149  prmirredlem  21501  dfprm2  21502  prmirred  21503  fermltlchr  21562  znfld  21597  freshmansdream  21611  frobrhm  21612  ply1fermltlchr  22332  rtprmirr  26818  wilthlem1  27126  wilthlem2  27127  wilthlem3  27128  chtf  27166  efchtcl  27169  isppw2  27173  vmappw  27174  vmaprm  27175  vmacl  27176  efvmacl  27178  muval1  27191  chtprm  27211  chtdif  27216  efchtdvds  27217  dvdsppwf1o  27244  sgmppw  27256  0sgmppw  27257  1sgmprm  27258  vmalelog  27264  chtleppi  27269  chtublem  27270  fsumvma2  27273  vmasum  27275  chpchtsum  27278  chpub  27279  mersenne  27286  perfect1  27287  perfect  27290  pcbcctr  27335  bpos1lem  27341  bposlem1  27343  bposlem2  27344  bposlem6  27348  lgslem1  27356  lgsval2lem  27366  lgsvalmod  27375  lgsmod  27382  lgsdirprm  27390  lgsne0  27394  lgsprme0  27398  lgsqrlem1  27405  lgsqrlem2  27406  lgsqrlem4  27408  lgsqr  27410  lgsqrmod  27411  lgsqrmodndvds  27412  gausslemma2dlem0c  27417  gausslemma2dlem0i  27423  gausslemma2dlem1a  27424  gausslemma2dlem5a  27429  gausslemma2dlem7  27432  gausslemma2d  27433  lgseisenlem1  27434  lgseisenlem2  27435  lgseisenlem3  27436  lgseisenlem4  27437  lgsquadlem1  27439  lgsquadlem3  27441  lgsquad2lem2  27444  lgsquad2  27445  m1lgs  27447  2lgslem1a  27450  2lgslem1c  27452  2lgs  27466  2sqlem3  27479  2sqlem8  27485  2sqlem11  27488  2sqblem  27490  2sqmod  27495  chtppilimlem1  27532  rplogsumlem2  27544  rpvmasumlem  27546  dchrisum0flblem1  27567  dchrisum0flblem2  27568  padicabvf  27690  ostth1  27692  ostth3  27697  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  fusgrhashclwwlkn  30108  clwlksndivn  30115  numclwwlk5  30417  numclwwlk6  30419  numclwwlk7  30420  numclwwlk8  30421  znfermltl  33374  ply1fermltl  33589  nn0prpwlem  36305  nn0prpw  36306  aks4d1p6  42063  aks4d1p8d1  42066  aks4d1p8d2  42067  aks4d1p8d3  42068  aks4d1p8  42069  aks6d1c1p2  42091  aks6d1c1p3  42092  aks6d1c1  42098  aks6d1c2p1  42100  aks6d1c2p2  42101  aks6d1c3  42105  aks6d1c4  42106  aks6d1c2lem4  42109  aks6d1c5lem1  42118  aks6d1c6lem3  42154  aks6d1c6lem4  42155  aks6d1c7lem1  42162  aks6d1c7  42166  aks5lem1  42168  aks5lem2  42169  aks5lem3a  42171  aks5lem8  42183  aks5  42186  nzprmdif  44315  etransclem41  46231  etransclem44  46234  etransclem47  46237  etransclem48  46238  odz2prm2pw  47488  fmtnoprmfac1lem  47489  fmtnoprmfac1  47490  fmtnoprmfac2  47492  prmdvdsfmtnof1lem2  47510  2pwp1prm  47514  sfprmdvdsmersenne  47528  lighneallem2  47531  lighneallem3  47532  lighneallem4  47535  lighneal  47536  perfectALTV  47648  gbepos  47683  gbowpos  47684  sbgoldbaltlem1  47704  ztprmneprm  48192