Theorem prmnn 16018

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3142   class class class wbr 5066  2_oc2o 8096   ≈ cen 8506  ℕcn 11638   ∥ cdvds 15607  ℙcprime 16015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-prm 16016

This theorem is referenced by:  prmz  16019  prmssnn  16020  0nprm  16022  2mulprm  16037  nprmdvds1  16050  isprm5  16051  coprm  16055  prmdvdsexpr  16061  prmndvdsfaclt  16067  cncongrprm  16069  phiprmpw  16113  fermltl  16121  prmdiv  16122  prmdiveq  16123  prmdivdiv  16124  m1dvdsndvds  16135  vfermltl  16138  vfermltlALT  16139  powm2modprm  16140  reumodprminv  16141  modprm0  16142  nnnn0modprm0  16143  modprmn0modprm0  16144  oddprm  16147  nnoddn2prm  16148  prm23lt5  16151  pcpremul  16180  pcdvdsb  16205  pcelnn  16206  pcidlem  16208  pcid  16209  pcdvdstr  16212  pcgcd1  16213  pcprmpw2  16218  dvdsprmpweqnn  16221  dvdsprmpweqle  16222  pcaddlem  16224  pcadd  16225  pcmptcl  16227  pcmpt  16228  pcmpt2  16229  pcfaclem  16234  pcfac  16235  pcbc  16236  expnprm  16238  oddprmdvds  16239  prmpwdvds  16240  pockthlem  16241  pockthg  16242  pockthi  16243  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  prmrec  16258  1arith  16263  4sqlem11  16291  4sqlem12  16292  4sqlem13  16293  4sqlem14  16294  4sqlem17  16297  4sqlem18  16298  4sqlem19  16299  prmdvdsprmo  16378  prmgaplem3  16389  prmgaplem4  16390  prmgaplem5  16391  prmgaplem6  16392  prmgaplem8  16394  cshwshashnsame  16437  cshwshash  16438  prmlem1a  16440  pgpfi1  18720  pgp0  18721  sylow1lem1  18723  sylow1lem3  18725  sylow1lem4  18726  sylow1lem5  18727  odcau  18729  pgpfi  18730  fislw  18750  sylow3lem6  18757  gexexlem  18972  prmcyg  19014  ablfac1lem  19190  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem3a  19198  pgpfac1lem3  19199  ablfaclem3  19209  prmgrpsimpgd  19236  prmirredlem  20640  dfprm2  20641  prmirred  20642  znfld  20707  wilthlem1  25645  wilthlem2  25646  wilthlem3  25647  chtf  25685  efchtcl  25688  isppw2  25692  vmappw  25693  vmaprm  25694  vmacl  25695  efvmacl  25697  muval1  25710  chtprm  25730  chtdif  25735  efchtdvds  25736  dvdsppwf1o  25763  sgmppw  25773  0sgmppw  25774  1sgmprm  25775  vmalelog  25781  chtleppi  25786  chtublem  25787  fsumvma2  25790  vmasum  25792  chpchtsum  25795  chpub  25796  mersenne  25803  perfect1  25804  perfect  25807  pcbcctr  25852  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem6  25865  lgslem1  25873  lgsval2lem  25883  lgsvalmod  25892  lgsmod  25899  lgsdirprm  25907  lgsne0  25911  lgsprme0  25915  lgsqrlem1  25922  lgsqrlem2  25923  lgsqrlem4  25925  lgsqr  25927  lgsqrmod  25928  lgsqrmodndvds  25929  gausslemma2dlem0c  25934  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  gausslemma2dlem5a  25946  gausslemma2dlem7  25949  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem3  25958  lgsquad2lem2  25961  lgsquad2  25962  m1lgs  25964  2lgslem1a  25967  2lgslem1c  25969  2lgs  25983  2sqlem3  25996  2sqlem8  26002  2sqlem11  26005  2sqblem  26007  2sqmod  26012  chtppilimlem1  26049  rplogsumlem2  26061  rpvmasumlem  26063  dchrisum0flblem1  26084  dchrisum0flblem2  26085  padicabvf  26207  ostth1  26209  ostth3  26214  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  fusgrhashclwwlkn  27858  clwlksndivn  27865  numclwwlk5  28167  numclwwlk6  28169  numclwwlk7  28170  numclwwlk8  28171  prmdvdsbc  30532  freshmansdream  30859  nn0prpwlem  33670  nn0prpw  33671  rtprmirr  39243  nzprmdif  40700  etransclem41  42609  etransclem44  42612  etransclem47  42615  etransclem48  42616  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  fmtnoprmfac2  43778  prmdvdsfmtnof1lem2  43796  2pwp1prm  43800  sfprmdvdsmersenne  43817  lighneallem2  43820  lighneallem3  43821  lighneallem4  43824  lighneal  43825  perfectALTV  43937  gbepos  43972  gbowpos  43973  sbgoldbaltlem1  43993  ztprmneprm  44444