Theorem prmnn 12374

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 12373	. 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 12040  ℙcprime 12371

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 12372

This theorem is referenced by:  prmz  12375  prmssnn  12376  nprmdvds1  12404  isprm5lem  12405  isprm5  12406  coprm  12408  euclemma  12410  prmdvdsexpr  12414  cncongrprm  12421  phiprmpw  12486  fermltl  12498  prmdiv  12499  prmdiveq  12500  prmdivdiv  12501  m1dvdsndvds  12513  vfermltl  12516  powm2modprm  12517  reumodprminv  12518  modprm0  12519  nnnn0modprm0  12520  modprmn0modprm0  12521  oddprm  12524  nnoddn2prm  12525  prm23lt5  12528  pcpremul  12558  pcdvdsb  12585  pcelnn  12586  pcidlem  12588  pcid  12589  pcdvdstr  12592  pcgcd1  12593  pcprmpw2  12598  dvdsprmpweqnn  12601  dvdsprmpweqle  12602  pcaddlem  12604  pcadd  12605  pcmptcl  12607  pcmpt  12608  pcmpt2  12609  pcfaclem  12614  pcfac  12615  pcbc  12616  expnprm  12618  oddprmdvds  12619  prmpwdvds  12620  pockthlem  12621  pockthg  12622  pockthi  12623  1arith  12632  4sqlem11  12666  4sqlem12  12667  4sqlem13m  12668  4sqlem14  12669  4sqlem17  12672  4sqlem18  12673  4sqlem19  12674  znidom  14361  wilthlem1  15394  dvdsppwf1o  15403  sgmppw  15406  0sgmppw  15407  1sgmprm  15408  mersenne  15411  perfect1  15412  perfect  15415  lgslem1  15419  lgslem4  15422  lgsval  15423  lgsval2lem  15429  lgsvalmod  15438  lgsmod  15445  lgsdirprm  15453  lgsne0  15457  lgsprme0  15461  gausslemma2dlem0c  15470  gausslemma2dlem1a  15477  gausslemma2dlem5a  15484  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisenlem4  15492  lgsquadlem1  15496  lgsquadlem3  15498  lgsquad2lem2  15501  lgsquad2  15502  m1lgs  15504  2lgslem1a  15507  2lgslem1c  15509  2lgs  15523  2sqlem3  15536  2sqlem8  15542