Theorem prmnn 12866

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

Syntax hints:   → wi 4   ∈ wcel 2209  {crab 2532   class class class wbr 4125  2_oc2o 6671   ≈ cen 7010  ℕcn 9283   ∥ cdvds 12532  ℙcprime 12863

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rab 2537  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126  df-prm 12864

This theorem is referenced by:  prmz  12867  prmssnn  12868  nprmdvds1  12896  isprm5lem  12897  isprm5  12898  coprm  12900  euclemma  12902  prmdvdsexpr  12906  cncongrprm  12913  phiprmpw  12978  fermltl  12990  prmdiv  12991  prmdiveq  12992  prmdivdiv  12993  m1dvdsndvds  13005  vfermltl  13008  powm2modprm  13009  reumodprminv  13010  modprm0  13011  nnnn0modprm0  13012  modprmn0modprm0  13013  oddprm  13016  nnoddn2prm  13017  prm23lt5  13020  pcpremul  13050  pcdvdsb  13077  pcelnn  13078  pcidlem  13080  pcid  13081  pcdvdstr  13084  pcgcd1  13085  pcprmpw2  13090  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  pcaddlem  13096  pcadd  13097  pcmptcl  13099  pcmpt  13100  pcmpt2  13101  pcfaclem  13106  pcfac  13107  pcbc  13108  expnprm  13110  oddprmdvds  13111  prmpwdvds  13112  pockthlem  13113  pockthg  13114  pockthi  13115  1arith  13124  4sqlem11  13158  4sqlem12  13159  4sqlem13m  13160  4sqlem14  13161  4sqlem17  13164  4sqlem18  13165  4sqlem19  13166  znidom  14964  wilthlem1  16008  dvdsppwf1o  16017  sgmppw  16020  0sgmppw  16021  1sgmprm  16022  mersenne  16025  perfect1  16026  perfect  16029  lgslem1  16033  lgslem4  16036  lgsval  16037  lgsval2lem  16043  lgsvalmod  16052  lgsmod  16059  lgsdirprm  16067  lgsne0  16071  lgsprme0  16075  gausslemma2dlem0c  16084  gausslemma2dlem1a  16091  gausslemma2dlem5a  16098  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem3  16112  lgsquad2lem2  16115  lgsquad2  16116  m1lgs  16118  2lgslem1a  16121  2lgslem1c  16123  2lgs  16137  2sqlem3  16150  2sqlem8  16156