Theorem prmnn 16893

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  {crab 3416   class class class wbr 5108  2_oc2o 8508   ≈ cen 9008  ℕcn 12375   ∥ cdvds 16466  ℙcprime 16890

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-prm 16891

This theorem is used by:  prmz  16894  prmssnn  16895  0nprm  16897  2mulprm  16912  nprmdvds1  16926  isprm5  16927  coprm  16931  prmdvdsexpr  16937  prmndvdsfaclt  16945  prmdvdsbc  16946  prmdvdsncoprmbd  16947  cncongrprm  16949  phiprmpw  16997  fermltl  17005  prmdiv  17006  prmdiveq  17007  prmdivdiv  17008  m1dvdsndvds  17020  vfermltl  17023  vfermltlALT  17024  powm2modprm  17025  reumodprminv  17026  modprm0  17027  nnnn0modprm0  17028  modprmn0modprm0  17029  oddprm  17032  nnoddn2prm  17033  prm23lt5  17036  pcpremul  17065  pcdvdsb  17091  pcelnn  17092  pcidlem  17094  pcid  17095  pcdvdstr  17098  pcgcd1  17099  pcprmpw2  17104  dvdsprmpweqnn  17107  dvdsprmpweqle  17108  pcaddlem  17110  pcadd  17111  pcmptcl  17113  pcmpt  17114  pcmpt2  17115  pcfaclem  17120  pcfac  17121  pcbc  17122  expnprm  17124  oddprmdvds  17125  prmpwdvds  17126  pockthlem  17127  pockthg  17128  pockthi  17129  prmreclem4  17141  prmreclem5  17142  prmreclem6  17143  prmrec  17144  1arith  17149  4sqlem11  17177  4sqlem12  17178  4sqlem13  17179  4sqlem14  17180  4sqlem17  17183  4sqlem18  17184  4sqlem19  17185  prmdvdsprmo  17264  prmgaplem3  17275  prmgaplem4  17276  prmgaplem5  17277  prmgaplem6  17278  prmgaplem8  17280  cshwshashnsame  17325  cshwshash  17326  prmlem1a  17328  pgpfi1  19860  pgp0  19861  sylow1lem1  19863  sylow1lem3  19865  sylow1lem4  19866  sylow1lem5  19867  odcau  19869  pgpfi  19870  fislw  19890  sylow3lem6  19897  gexexlem  20117  prmcyg  20159  ablfac1lem  20335  ablfac1b  20337  ablfac1eu  20340  pgpfac1lem3a  20343  pgpfac1lem3  20344  ablfaclem3  20354  prmgrpsimpgd  20381  prmirredlem  21833  dfprm2  21834  prmirred  21835  fermltlchr  21890  znfld  21921  freshmansdream  21935  frobrhm  21936  ply1fermltlchr  22685  rtprmirr  27145  wilthlem1  27452  wilthlem2  27453  wilthlem3  27454  chtf  27492  efchtcl  27495  isppw2  27499  vmappw  27500  vmaprm  27501  vmacl  27502  efvmacl  27504  muval1  27517  chtprm  27537  chtdif  27542  efchtdvds  27543  dvdsppwf1o  27570  sgmppw  27581  0sgmppw  27582  1sgmprm  27583  vmalelog  27589  chtleppi  27594  chtublem  27595  fsumvma2  27598  vmasum  27600  chpchtsum  27603  chpub  27604  mersenne  27611  perfect1  27612  perfect  27615  pcbcctr  27660  bpos1lem  27666  bposlem1  27668  bposlem2  27669  bposlem6  27673  lgslem1  27681  lgsval2lem  27691  lgsvalmod  27700  lgsmod  27707  lgsdirprm  27715  lgsne0  27719  lgsprme0  27723  lgsqrlem1  27730  lgsqrlem2  27731  lgsqrlem4  27733  lgsqr  27735  lgsqrmod  27736  lgsqrmodndvds  27737  gausslemma2dlem0c  27742  gausslemma2dlem0i  27748  gausslemma2dlem1a  27749  gausslemma2dlem5a  27754  gausslemma2dlem7  27757  gausslemma2d  27758  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgsquadlem1  27764  lgsquadlem3  27766  lgsquad2lem2  27769  lgsquad2  27770  m1lgs  27772  2lgslem1a  27775  2lgslem1c  27777  2lgs  27791  2sqlem3  27804  2sqlem8  27810  2sqlem11  27813  2sqblem  27815  2sqmod  27820  chtppilimlem1  27857  rplogsumlem2  27869  rpvmasumlem  27871  dchrisum0flblem1  27892  dchrisum0flblem2  27893  padicabvf  28015  ostth1  28017  ostth3  28022  fltoprm  28052  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  fusgrhashclwwlkn  30727  clwlksndivn  30734  numclwwlk5  31046  numclwwlk6  31048  numclwwlk7  31049  numclwwlk8  31050  znfermltl  34026  ply1fermltl  34221  cos9thpiminplylem2  34526  nn0prpwlem  37325  nn0prpw  37326  aks4d1p6  43397  aks4d1p8d1  43400  aks4d1p8d2  43401  aks4d1p8d3  43402  aks4d1p8  43403  aks6d1c1p2  43425  aks6d1c1p3  43426  aks6d1c1  43432  aks6d1c2p1  43434  aks6d1c2p2  43435  aks6d1c3  43439  aks6d1c4  43440  aks6d1c2lem4  43443  aks6d1c5lem1  43452  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c7lem1  43496  aks6d1c7  43500  aks5lem1  43502  aks5lem2  43503  aks5lem3a  43505  aks5lem8  43517  aks5  43520  nzprmdif  45564  etransclem41  47558  etransclem44  47561  etransclem47  47564  etransclem48  47565  odz2prm2pw  48921  fmtnoprmfac1lem  48922  fmtnoprmfac1  48923  fmtnoprmfac2  48925  prmdvdsfmtnof1lem2  48943  2pwp1prm  48947  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem3  48965  lighneallem4  48968  lighneal  48969  perfectALTV  49094  gbepos  49129  gbowpos  49130  sbgoldbaltlem1  49150  ztprmneprm  49790