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  16094  dvdsppwf1o  16103  sgmppw  16106  0sgmppw  16107  1sgmprm  16108  mersenne  16111  perfect1  16112  perfect  16115  lgslem1  16119  lgslem4  16122  lgsval  16123  lgsval2lem  16129  lgsvalmod  16138  lgsmod  16145  lgsdirprm  16153  lgsne0  16157  lgsprme0  16161  gausslemma2dlem0c  16170  gausslemma2dlem1a  16177  gausslemma2dlem5a  16184  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem3  16198  lgsquad2lem2  16201  lgsquad2  16202  m1lgs  16204  2lgslem1a  16207  2lgslem1c  16209  2lgs  16223  2sqlem3  16236  2sqlem8  16242