Theorem prmnn 12681

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

Syntax hints:   → wi 4   ∈ wcel 2202  {crab 2514   class class class wbr 4088  2_oc2o 6575   ≈ cen 6906  ℕcn 9142   ∥ cdvds 12347  ℙcprime 12678

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-prm 12679

This theorem is referenced by:  prmz  12682  prmssnn  12683  nprmdvds1  12711  isprm5lem  12712  isprm5  12713  coprm  12715  euclemma  12717  prmdvdsexpr  12721  cncongrprm  12728  phiprmpw  12793  fermltl  12805  prmdiv  12806  prmdiveq  12807  prmdivdiv  12808  m1dvdsndvds  12820  vfermltl  12823  powm2modprm  12824  reumodprminv  12825  modprm0  12826  nnnn0modprm0  12827  modprmn0modprm0  12828  oddprm  12831  nnoddn2prm  12832  prm23lt5  12835  pcpremul  12865  pcdvdsb  12892  pcelnn  12893  pcidlem  12895  pcid  12896  pcdvdstr  12899  pcgcd1  12900  pcprmpw2  12905  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  pcaddlem  12911  pcadd  12912  pcmptcl  12914  pcmpt  12915  pcmpt2  12916  pcfaclem  12921  pcfac  12922  pcbc  12923  expnprm  12925  oddprmdvds  12926  prmpwdvds  12927  pockthlem  12928  pockthg  12929  pockthi  12930  1arith  12939  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  4sqlem19  12981  znidom  14670  wilthlem1  15703  dvdsppwf1o  15712  sgmppw  15715  0sgmppw  15716  1sgmprm  15717  mersenne  15720  perfect1  15721  perfect  15724  lgslem1  15728  lgslem4  15731  lgsval  15732  lgsval2lem  15738  lgsvalmod  15747  lgsmod  15754  lgsdirprm  15762  lgsne0  15766  lgsprme0  15770  gausslemma2dlem0c  15779  gausslemma2dlem1a  15786  gausslemma2dlem5a  15793  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem3  15807  lgsquad2lem2  15810  lgsquad2  15811  m1lgs  15813  2lgslem1a  15816  2lgslem1c  15818  2lgs  15832  2sqlem3  15845  2sqlem8  15851