Theorem prmnn 16644

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

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3405   class class class wbr 5107  2_oc2o 8428   ≈ cen 8915  ℕcn 12186   ∥ cdvds 16222  ℙcprime 16641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-prm 16642

This theorem is referenced by:  prmz  16645  prmssnn  16646  0nprm  16648  2mulprm  16663  nprmdvds1  16676  isprm5  16677  coprm  16681  prmdvdsexpr  16687  prmndvdsfaclt  16695  prmdvdsbc  16696  prmdvdsncoprmbd  16697  cncongrprm  16699  phiprmpw  16746  fermltl  16754  prmdiv  16755  prmdiveq  16756  prmdivdiv  16757  m1dvdsndvds  16769  vfermltl  16772  vfermltlALT  16773  powm2modprm  16774  reumodprminv  16775  modprm0  16776  nnnn0modprm0  16777  modprmn0modprm0  16778  oddprm  16781  nnoddn2prm  16782  prm23lt5  16785  pcpremul  16814  pcdvdsb  16840  pcelnn  16841  pcidlem  16843  pcid  16844  pcdvdstr  16847  pcgcd1  16848  pcprmpw2  16853  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcaddlem  16859  pcadd  16860  pcmptcl  16862  pcmpt  16863  pcmpt2  16864  pcfaclem  16869  pcfac  16870  pcbc  16871  expnprm  16873  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  pockthi  16878  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  1arith  16898  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  4sqlem19  16934  prmdvdsprmo  17013  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem8  17029  cshwshashnsame  17074  cshwshash  17075  prmlem1a  17077  pgpfi1  19525  pgp0  19526  sylow1lem1  19528  sylow1lem3  19530  sylow1lem4  19531  sylow1lem5  19532  odcau  19534  pgpfi  19535  fislw  19555  sylow3lem6  19562  gexexlem  19782  prmcyg  19824  ablfac1lem  20000  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem3a  20008  pgpfac1lem3  20009  ablfaclem3  20019  prmgrpsimpgd  20046  prmirredlem  21382  dfprm2  21383  prmirred  21384  fermltlchr  21439  znfld  21470  freshmansdream  21484  frobrhm  21485  ply1fermltlchr  22199  rtprmirr  26670  wilthlem1  26978  wilthlem2  26979  wilthlem3  26980  chtf  27018  efchtcl  27021  isppw2  27025  vmappw  27026  vmaprm  27027  vmacl  27028  efvmacl  27030  muval1  27043  chtprm  27063  chtdif  27068  efchtdvds  27069  dvdsppwf1o  27096  sgmppw  27108  0sgmppw  27109  1sgmprm  27110  vmalelog  27116  chtleppi  27121  chtublem  27122  fsumvma2  27125  vmasum  27127  chpchtsum  27130  chpub  27131  mersenne  27138  perfect1  27139  perfect  27142  pcbcctr  27187  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem6  27200  lgslem1  27208  lgsval2lem  27218  lgsvalmod  27227  lgsmod  27234  lgsdirprm  27242  lgsne0  27246  lgsprme0  27250  lgsqrlem1  27257  lgsqrlem2  27258  lgsqrlem4  27260  lgsqr  27262  lgsqrmod  27263  lgsqrmodndvds  27264  gausslemma2dlem0c  27269  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  gausslemma2dlem5a  27281  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem3  27293  lgsquad2lem2  27296  lgsquad2  27297  m1lgs  27299  2lgslem1a  27302  2lgslem1c  27304  2lgs  27318  2sqlem3  27331  2sqlem8  27337  2sqlem11  27340  2sqblem  27342  2sqmod  27347  chtppilimlem1  27384  rplogsumlem2  27396  rpvmasumlem  27398  dchrisum0flblem1  27419  dchrisum0flblem2  27420  padicabvf  27542  ostth1  27544  ostth3  27549  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  fusgrhashclwwlkn  30008  clwlksndivn  30015  numclwwlk5  30317  numclwwlk6  30319  numclwwlk7  30320  numclwwlk8  30321  znfermltl  33337  ply1fermltl  33553  cos9thpiminplylem2  33773  nn0prpwlem  36310  nn0prpw  36311  aks4d1p6  42069  aks4d1p8d1  42072  aks4d1p8d2  42073  aks4d1p8d3  42074  aks4d1p8  42075  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1  42104  aks6d1c2p1  42106  aks6d1c2p2  42107  aks6d1c3  42111  aks6d1c4  42112  aks6d1c2lem4  42115  aks6d1c5lem1  42124  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7  42172  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  aks5lem8  42189  aks5  42192  nzprmdif  44308  etransclem41  46273  etransclem44  46276  etransclem47  46279  etransclem48  46280  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  fmtnoprmfac2  47568  prmdvdsfmtnof1lem2  47586  2pwp1prm  47590  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  lighneal  47612  perfectALTV  47724  gbepos  47759  gbowpos  47760  sbgoldbaltlem1  47780  ztprmneprm  48335