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 500	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2142  {crab 3414   class class class wbr 5100  2_oc2o 8431   ≈ cen 8924  ℕcn 12210   ∥ cdvds 16286  ℙcprime 16705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-prm 16706

This theorem is referenced by:  prmz  16709  prmssnn  16710  0nprm  16712  2mulprm  16727  nprmdvds1  16741  isprm5  16742  coprm  16746  prmdvdsexpr  16752  prmndvdsfaclt  16760  prmdvdsbc  16761  prmdvdsncoprmbd  16762  cncongrprm  16764  phiprmpw  16811  fermltl  16819  prmdiv  16820  prmdiveq  16821  prmdivdiv  16822  m1dvdsndvds  16834  vfermltl  16837  vfermltlALT  16838  powm2modprm  16839  reumodprminv  16840  modprm0  16841  nnnn0modprm0  16842  modprmn0modprm0  16843  oddprm  16846  nnoddn2prm  16847  prm23lt5  16850  pcpremul  16879  pcdvdsb  16905  pcelnn  16906  pcidlem  16908  pcid  16909  pcdvdstr  16912  pcgcd1  16913  pcprmpw2  16918  dvdsprmpweqnn  16921  dvdsprmpweqle  16922  pcaddlem  16924  pcadd  16925  pcmptcl  16927  pcmpt  16928  pcmpt2  16929  pcfaclem  16934  pcfac  16935  pcbc  16936  expnprm  16938  oddprmdvds  16939  prmpwdvds  16940  pockthlem  16941  pockthg  16942  pockthi  16943  prmreclem4  16955  prmreclem5  16956  prmreclem6  16957  prmrec  16958  1arith  16963  4sqlem11  16991  4sqlem12  16992  4sqlem13  16993  4sqlem14  16994  4sqlem17  16997  4sqlem18  16998  4sqlem19  16999  prmdvdsprmo  17078  prmgaplem3  17089  prmgaplem4  17090  prmgaplem5  17091  prmgaplem6  17092  prmgaplem8  17094  cshwshashnsame  17139  cshwshash  17140  prmlem1a  17142  pgpfi1  19635  pgp0  19636  sylow1lem1  19638  sylow1lem3  19640  sylow1lem4  19641  sylow1lem5  19642  odcau  19644  pgpfi  19645  fislw  19665  sylow3lem6  19672  gexexlem  19892  prmcyg  19934  ablfac1lem  20110  ablfac1b  20112  ablfac1eu  20115  pgpfac1lem3a  20118  pgpfac1lem3  20119  ablfaclem3  20129  prmgrpsimpgd  20156  prmirredlem  21521  dfprm2  21522  prmirred  21523  fermltlchr  21578  znfld  21609  freshmansdream  21623  frobrhm  21624  ply1fermltlchr  22372  rtprmirr  26822  wilthlem1  27129  wilthlem2  27130  wilthlem3  27131  chtf  27169  efchtcl  27172  isppw2  27176  vmappw  27177  vmaprm  27178  vmacl  27179  efvmacl  27181  muval1  27194  chtprm  27214  chtdif  27219  efchtdvds  27220  dvdsppwf1o  27247  sgmppw  27258  0sgmppw  27259  1sgmprm  27260  vmalelog  27266  chtleppi  27271  chtublem  27272  fsumvma2  27275  vmasum  27277  chpchtsum  27280  chpub  27281  mersenne  27288  perfect1  27289  perfect  27292  pcbcctr  27337  bpos1lem  27343  bposlem1  27345  bposlem2  27346  bposlem6  27350  lgslem1  27358  lgsval2lem  27368  lgsvalmod  27377  lgsmod  27384  lgsdirprm  27392  lgsne0  27396  lgsprme0  27400  lgsqrlem1  27407  lgsqrlem2  27408  lgsqrlem4  27410  lgsqr  27412  lgsqrmod  27413  lgsqrmodndvds  27414  gausslemma2dlem0c  27419  gausslemma2dlem0i  27425  gausslemma2dlem1a  27426  gausslemma2dlem5a  27431  gausslemma2dlem7  27434  gausslemma2d  27435  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgseisenlem4  27439  lgsquadlem1  27441  lgsquadlem3  27443  lgsquad2lem2  27446  lgsquad2  27447  m1lgs  27449  2lgslem1a  27452  2lgslem1c  27454  2lgs  27468  2sqlem3  27481  2sqlem8  27487  2sqlem11  27490  2sqblem  27492  2sqmod  27497  chtppilimlem1  27534  rplogsumlem2  27546  rpvmasumlem  27548  dchrisum0flblem1  27569  dchrisum0flblem2  27570  padicabvf  27692  ostth1  27694  ostth3  27699  hashecclwwlkn1  30276  umgrhashecclwwlk  30277  fusgrhashclwwlkn  30278  clwlksndivn  30285  numclwwlk5  30587  numclwwlk6  30589  numclwwlk7  30590  numclwwlk8  30591  znfermltl  33549  ply1fermltl  33779  cos9thpiminplylem2  34077  nn0prpwlem  36679  nn0prpw  36680  aks4d1p6  42695  aks4d1p8d1  42698  aks4d1p8d2  42699  aks4d1p8d3  42700  aks4d1p8  42701  aks6d1c1p2  42723  aks6d1c1p3  42724  aks6d1c1  42730  aks6d1c2p1  42732  aks6d1c2p2  42733  aks6d1c3  42737  aks6d1c4  42738  aks6d1c2lem4  42741  aks6d1c5lem1  42750  aks6d1c6lem3  42786  aks6d1c6lem4  42787  aks6d1c7lem1  42794  aks6d1c7  42798  aks5lem1  42800  aks5lem2  42801  aks5lem3a  42803  aks5lem8  42815  aks5  42818  nzprmdif  44892  etransclem41  46846  etransclem44  46849  etransclem47  46852  etransclem48  46853  odz2prm2pw  48169  fmtnoprmfac1lem  48170  fmtnoprmfac1  48171  fmtnoprmfac2  48173  prmdvdsfmtnof1lem2  48191  2pwp1prm  48195  sfprmdvdsmersenne  48209  lighneallem2  48212  lighneallem3  48213  lighneallem4  48216  lighneal  48217  perfectALTV  48342  gbepos  48377  gbowpos  48378  sbgoldbaltlem1  48398  ztprmneprm  48966