Theorem prmnn 12807

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

Syntax hints:   → wi 4   ∈ wcel 2203  {crab 2524   class class class wbr 4109  2_oc2o 6641   ≈ cen 6973  ℕcn 9237   ∥ cdvds 12473  ℙcprime 12804

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rab 2529  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-prm 12805

This theorem is referenced by:  prmz  12808  prmssnn  12809  nprmdvds1  12837  isprm5lem  12838  isprm5  12839  coprm  12841  euclemma  12843  prmdvdsexpr  12847  cncongrprm  12854  phiprmpw  12919  fermltl  12931  prmdiv  12932  prmdiveq  12933  prmdivdiv  12934  m1dvdsndvds  12946  vfermltl  12949  powm2modprm  12950  reumodprminv  12951  modprm0  12952  nnnn0modprm0  12953  modprmn0modprm0  12954  oddprm  12957  nnoddn2prm  12958  prm23lt5  12961  pcpremul  12991  pcdvdsb  13018  pcelnn  13019  pcidlem  13021  pcid  13022  pcdvdstr  13025  pcgcd1  13026  pcprmpw2  13031  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  pcaddlem  13037  pcadd  13038  pcmptcl  13040  pcmpt  13041  pcmpt2  13042  pcfaclem  13047  pcfac  13048  pcbc  13049  expnprm  13051  oddprmdvds  13052  prmpwdvds  13053  pockthlem  13054  pockthg  13055  pockthi  13056  1arith  13065  4sqlem11  13099  4sqlem12  13100  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  4sqlem19  13107  znidom  14805  wilthlem1  15848  dvdsppwf1o  15857  sgmppw  15860  0sgmppw  15861  1sgmprm  15862  mersenne  15865  perfect1  15866  perfect  15869  lgslem1  15873  lgslem4  15876  lgsval  15877  lgsval2lem  15883  lgsvalmod  15892  lgsmod  15899  lgsdirprm  15907  lgsne0  15911  lgsprme0  15915  gausslemma2dlem0c  15924  gausslemma2dlem1a  15931  gausslemma2dlem5a  15938  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem3  15952  lgsquad2lem2  15955  lgsquad2  15956  m1lgs  15958  2lgslem1a  15961  2lgslem1c  15963  2lgs  15977  2sqlem3  15990  2sqlem8  15996