Theorem prmnn 12888

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  {crab 2532   class class class wbr 4130  2_oc2o 6681   ≈ cen 7020  ℕcn 9304   ∥ cdvds 12554  ℙcprime 12885

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-br 4131  df-prm 12886

This theorem is used by:  prmz  12889  prmssnn  12890  nprmdvds1  12918  isprm5lem  12919  isprm5  12920  coprm  12922  euclemma  12924  prmdvdsexpr  12928  cncongrprm  12935  phiprmpw  13000  fermltl  13012  prmdiv  13013  prmdiveq  13014  prmdivdiv  13015  m1dvdsndvds  13027  vfermltl  13030  powm2modprm  13031  reumodprminv  13032  modprm0  13033  nnnn0modprm0  13034  modprmn0modprm0  13035  oddprm  13038  nnoddn2prm  13039  prm23lt5  13042  pcpremul  13072  pcdvdsb  13099  pcelnn  13100  pcidlem  13102  pcid  13103  pcdvdstr  13106  pcgcd1  13107  pcprmpw2  13112  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  pcaddlem  13118  pcadd  13119  pcmptcl  13121  pcmpt  13122  pcmpt2  13123  pcfaclem  13128  pcfac  13129  pcbc  13130  expnprm  13132  oddprmdvds  13133  prmpwdvds  13134  pockthlem  13135  pockthg  13136  pockthi  13137  1arith  13146  4sqlem11  13180  4sqlem12  13181  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  4sqlem18  13187  4sqlem19  13188  znidom  14992  wilthlem1  16098  dvdsppwf1o  16107  sgmppw  16110  0sgmppw  16111  1sgmprm  16112  mersenne  16115  perfect1  16116  perfect  16119  lgslem1  16123  lgslem4  16126  lgsval  16127  lgsval2lem  16133  lgsvalmod  16142  lgsmod  16149  lgsdirprm  16157  lgsne0  16161  lgsprme0  16165  gausslemma2dlem0c  16174  gausslemma2dlem1a  16181  gausslemma2dlem5a  16188  lgseisenlem1  16193  lgseisenlem2  16194  lgseisenlem3  16195  lgseisenlem4  16196  lgsquadlem1  16200  lgsquadlem3  16202  lgsquad2lem2  16205  lgsquad2  16206  m1lgs  16208  2lgslem1a  16211  2lgslem1c  16213  2lgs  16227  2sqlem3  16240  2sqlem8  16246