Theorem prmnn 12248

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

Syntax hints:   → wi 4   ∈ wcel 2164  {crab 2476   class class class wbr 4029  2_oc2o 6463   ≈ cen 6792  ℕcn 8982   ∥ cdvds 11930  ℙcprime 12245

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rab 2481  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030  df-prm 12246

This theorem is referenced by:  prmz  12249  prmssnn  12250  nprmdvds1  12278  isprm5lem  12279  isprm5  12280  coprm  12282  euclemma  12284  prmdvdsexpr  12288  cncongrprm  12295  phiprmpw  12360  fermltl  12372  prmdiv  12373  prmdiveq  12374  prmdivdiv  12375  m1dvdsndvds  12386  vfermltl  12389  powm2modprm  12390  reumodprminv  12391  modprm0  12392  nnnn0modprm0  12393  modprmn0modprm0  12394  oddprm  12397  nnoddn2prm  12398  prm23lt5  12401  pcpremul  12431  pcdvdsb  12458  pcelnn  12459  pcidlem  12461  pcid  12462  pcdvdstr  12465  pcgcd1  12466  pcprmpw2  12471  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  pcaddlem  12477  pcadd  12478  pcmptcl  12480  pcmpt  12481  pcmpt2  12482  pcfaclem  12487  pcfac  12488  pcbc  12489  expnprm  12491  oddprmdvds  12492  prmpwdvds  12493  pockthlem  12494  pockthg  12495  pockthi  12496  1arith  12505  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  4sqlem19  12547  znidom  14145  wilthlem1  15112  lgslem1  15116  lgslem4  15119  lgsval  15120  lgsval2lem  15126  lgsvalmod  15135  lgsmod  15142  lgsdirprm  15150  lgsne0  15154  lgsprme0  15158  gausslemma2dlem0c  15167  gausslemma2dlem1a  15174  gausslemma2dlem5a  15181  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem3  15204  2sqlem8  15210