Theorem prmnn 12647

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

Syntax hints:   → wi 4   ∈ wcel 2200  {crab 2512   class class class wbr 4083  2_oc2o 6562   ≈ cen 6893  ℕcn 9121   ∥ cdvds 12313  ℙcprime 12644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-prm 12645

This theorem is referenced by:  prmz  12648  prmssnn  12649  nprmdvds1  12677  isprm5lem  12678  isprm5  12679  coprm  12681  euclemma  12683  prmdvdsexpr  12687  cncongrprm  12694  phiprmpw  12759  fermltl  12771  prmdiv  12772  prmdiveq  12773  prmdivdiv  12774  m1dvdsndvds  12786  vfermltl  12789  powm2modprm  12790  reumodprminv  12791  modprm0  12792  nnnn0modprm0  12793  modprmn0modprm0  12794  oddprm  12797  nnoddn2prm  12798  prm23lt5  12801  pcpremul  12831  pcdvdsb  12858  pcelnn  12859  pcidlem  12861  pcid  12862  pcdvdstr  12865  pcgcd1  12866  pcprmpw2  12871  dvdsprmpweqnn  12874  dvdsprmpweqle  12875  pcaddlem  12877  pcadd  12878  pcmptcl  12880  pcmpt  12881  pcmpt2  12882  pcfaclem  12887  pcfac  12888  pcbc  12889  expnprm  12891  oddprmdvds  12892  prmpwdvds  12893  pockthlem  12894  pockthg  12895  pockthi  12896  1arith  12905  4sqlem11  12939  4sqlem12  12940  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  4sqlem18  12946  4sqlem19  12947  znidom  14636  wilthlem1  15669  dvdsppwf1o  15678  sgmppw  15681  0sgmppw  15682  1sgmprm  15683  mersenne  15686  perfect1  15687  perfect  15690  lgslem1  15694  lgslem4  15697  lgsval  15698  lgsval2lem  15704  lgsvalmod  15713  lgsmod  15720  lgsdirprm  15728  lgsne0  15732  lgsprme0  15736  gausslemma2dlem0c  15745  gausslemma2dlem1a  15752  gausslemma2dlem5a  15759  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem3  15773  lgsquad2lem2  15776  lgsquad2  15777  m1lgs  15779  2lgslem1a  15782  2lgslem1c  15784  2lgs  15798  2sqlem3  15811  2sqlem8  15817