Theorem prmnn 16754

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {crab 3418   class class class wbr 5111  2_oc2o 8453   ≈ cen 8946  ℕcn 12248   ∥ cdvds 16332  ℙcprime 16751

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-prm 16752

This theorem is used by:  prmz  16755  prmssnn  16756  0nprm  16758  2mulprm  16773  nprmdvds1  16787  isprm5  16788  coprm  16792  prmdvdsexpr  16798  prmndvdsfaclt  16806  prmdvdsbc  16807  prmdvdsncoprmbd  16808  cncongrprm  16810  phiprmpw  16857  fermltl  16865  prmdiv  16866  prmdiveq  16867  prmdivdiv  16868  m1dvdsndvds  16880  vfermltl  16883  vfermltlALT  16884  powm2modprm  16885  reumodprminv  16886  modprm0  16887  nnnn0modprm0  16888  modprmn0modprm0  16889  oddprm  16892  nnoddn2prm  16893  prm23lt5  16896  pcpremul  16925  pcdvdsb  16951  pcelnn  16952  pcidlem  16954  pcid  16955  pcdvdstr  16958  pcgcd1  16959  pcprmpw2  16964  dvdsprmpweqnn  16967  dvdsprmpweqle  16968  pcaddlem  16970  pcadd  16971  pcmptcl  16973  pcmpt  16974  pcmpt2  16975  pcfaclem  16980  pcfac  16981  pcbc  16982  expnprm  16984  oddprmdvds  16985  prmpwdvds  16986  pockthlem  16987  pockthg  16988  pockthi  16989  prmreclem4  17001  prmreclem5  17002  prmreclem6  17003  prmrec  17004  1arith  17009  4sqlem11  17037  4sqlem12  17038  4sqlem13  17039  4sqlem14  17040  4sqlem17  17043  4sqlem18  17044  4sqlem19  17045  prmdvdsprmo  17124  prmgaplem3  17135  prmgaplem4  17136  prmgaplem5  17137  prmgaplem6  17138  prmgaplem8  17140  cshwshashnsame  17185  cshwshash  17186  prmlem1a  17188  pgpfi1  19709  pgp0  19710  sylow1lem1  19712  sylow1lem3  19714  sylow1lem4  19715  sylow1lem5  19716  odcau  19718  pgpfi  19719  fislw  19739  sylow3lem6  19746  gexexlem  19966  prmcyg  20008  ablfac1lem  20184  ablfac1b  20186  ablfac1eu  20189  pgpfac1lem3a  20192  pgpfac1lem3  20193  ablfaclem3  20203  prmgrpsimpgd  20230  prmirredlem  21672  dfprm2  21673  prmirred  21674  fermltlchr  21729  znfld  21760  freshmansdream  21774  frobrhm  21775  ply1fermltlchr  22522  rtprmirr  26976  wilthlem1  27283  wilthlem2  27284  wilthlem3  27285  chtf  27323  efchtcl  27326  isppw2  27330  vmappw  27331  vmaprm  27332  vmacl  27333  efvmacl  27335  muval1  27348  chtprm  27368  chtdif  27373  efchtdvds  27374  dvdsppwf1o  27401  sgmppw  27412  0sgmppw  27413  1sgmprm  27414  vmalelog  27420  chtleppi  27425  chtublem  27426  fsumvma2  27429  vmasum  27431  chpchtsum  27434  chpub  27435  mersenne  27442  perfect1  27443  perfect  27446  pcbcctr  27491  bpos1lem  27497  bposlem1  27499  bposlem2  27500  bposlem6  27504  lgslem1  27512  lgsval2lem  27522  lgsvalmod  27531  lgsmod  27538  lgsdirprm  27546  lgsne0  27550  lgsprme0  27554  lgsqrlem1  27561  lgsqrlem2  27562  lgsqrlem4  27564  lgsqr  27566  lgsqrmod  27567  lgsqrmodndvds  27568  gausslemma2dlem0c  27573  gausslemma2dlem0i  27579  gausslemma2dlem1a  27580  gausslemma2dlem5a  27585  gausslemma2dlem7  27588  gausslemma2d  27589  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem3  27592  lgseisenlem4  27593  lgsquadlem1  27595  lgsquadlem3  27597  lgsquad2lem2  27600  lgsquad2  27601  m1lgs  27603  2lgslem1a  27606  2lgslem1c  27608  2lgs  27622  2sqlem3  27635  2sqlem8  27641  2sqlem11  27644  2sqblem  27646  2sqmod  27651  chtppilimlem1  27688  rplogsumlem2  27700  rpvmasumlem  27702  dchrisum0flblem1  27723  dchrisum0flblem2  27724  padicabvf  27846  ostth1  27848  ostth3  27853  hashecclwwlkn1  30495  umgrhashecclwwlk  30496  fusgrhashclwwlkn  30497  clwlksndivn  30504  numclwwlk5  30810  numclwwlk6  30812  numclwwlk7  30813  numclwwlk8  30814  znfermltl  33745  ply1fermltl  33940  cos9thpiminplylem2  34237  nn0prpwlem  36890  nn0prpw  36891  aks4d1p6  42906  aks4d1p8d1  42909  aks4d1p8d2  42910  aks4d1p8d3  42911  aks4d1p8  42912  aks6d1c1p2  42934  aks6d1c1p3  42935  aks6d1c1  42941  aks6d1c2p1  42943  aks6d1c2p2  42944  aks6d1c3  42948  aks6d1c4  42949  aks6d1c2lem4  42952  aks6d1c5lem1  42961  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c7lem1  43005  aks6d1c7  43009  aks5lem1  43011  aks5lem2  43012  aks5lem3a  43014  aks5lem8  43026  aks5  43029  nzprmdif  45087  etransclem41  47047  etransclem44  47050  etransclem47  47053  etransclem48  47054  odz2prm2pw  48373  fmtnoprmfac1lem  48374  fmtnoprmfac1  48375  fmtnoprmfac2  48377  prmdvdsfmtnof1lem2  48395  2pwp1prm  48399  sfprmdvdsmersenne  48413  lighneallem2  48416  lighneallem3  48417  lighneallem4  48420  lighneal  48421  perfectALTV  48546  gbepos  48581  gbowpos  48582  sbgoldbaltlem1  48602  ztprmneprm  49184