Theorem prmnn 12403

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

Syntax hints:   → wi 4   ∈ wcel 2175  {crab 2487   class class class wbr 4043  2_oc2o 6495   ≈ cen 6824  ℕcn 9035   ∥ cdvds 12069  ℙcprime 12400

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rab 2492  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044  df-prm 12401

This theorem is referenced by:  prmz  12404  prmssnn  12405  nprmdvds1  12433  isprm5lem  12434  isprm5  12435  coprm  12437  euclemma  12439  prmdvdsexpr  12443  cncongrprm  12450  phiprmpw  12515  fermltl  12527  prmdiv  12528  prmdiveq  12529  prmdivdiv  12530  m1dvdsndvds  12542  vfermltl  12545  powm2modprm  12546  reumodprminv  12547  modprm0  12548  nnnn0modprm0  12549  modprmn0modprm0  12550  oddprm  12553  nnoddn2prm  12554  prm23lt5  12557  pcpremul  12587  pcdvdsb  12614  pcelnn  12615  pcidlem  12617  pcid  12618  pcdvdstr  12621  pcgcd1  12622  pcprmpw2  12627  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  pcaddlem  12633  pcadd  12634  pcmptcl  12636  pcmpt  12637  pcmpt2  12638  pcfaclem  12643  pcfac  12644  pcbc  12645  expnprm  12647  oddprmdvds  12648  prmpwdvds  12649  pockthlem  12650  pockthg  12651  pockthi  12652  1arith  12661  4sqlem11  12695  4sqlem12  12696  4sqlem13m  12697  4sqlem14  12698  4sqlem17  12701  4sqlem18  12702  4sqlem19  12703  znidom  14390  wilthlem1  15423  dvdsppwf1o  15432  sgmppw  15435  0sgmppw  15436  1sgmprm  15437  mersenne  15440  perfect1  15441  perfect  15444  lgslem1  15448  lgslem4  15451  lgsval  15452  lgsval2lem  15458  lgsvalmod  15467  lgsmod  15474  lgsdirprm  15482  lgsne0  15486  lgsprme0  15490  gausslemma2dlem0c  15499  gausslemma2dlem1a  15506  gausslemma2dlem5a  15513  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgsquadlem1  15525  lgsquadlem3  15527  lgsquad2lem2  15530  lgsquad2  15531  m1lgs  15533  2lgslem1a  15536  2lgslem1c  15538  2lgs  15552  2sqlem3  15565  2sqlem8  15571