Theorem prmnn 12672

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

Syntax hints:   → wi 4   ∈ wcel 2200  {crab 2512   class class class wbr 4086  2_oc2o 6571   ≈ cen 6902  ℕcn 9133   ∥ cdvds 12338  ℙcprime 12669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rab 2517  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-prm 12670

This theorem is referenced by:  prmz  12673  prmssnn  12674  nprmdvds1  12702  isprm5lem  12703  isprm5  12704  coprm  12706  euclemma  12708  prmdvdsexpr  12712  cncongrprm  12719  phiprmpw  12784  fermltl  12796  prmdiv  12797  prmdiveq  12798  prmdivdiv  12799  m1dvdsndvds  12811  vfermltl  12814  powm2modprm  12815  reumodprminv  12816  modprm0  12817  nnnn0modprm0  12818  modprmn0modprm0  12819  oddprm  12822  nnoddn2prm  12823  prm23lt5  12826  pcpremul  12856  pcdvdsb  12883  pcelnn  12884  pcidlem  12886  pcid  12887  pcdvdstr  12890  pcgcd1  12891  pcprmpw2  12896  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  pcaddlem  12902  pcadd  12903  pcmptcl  12905  pcmpt  12906  pcmpt2  12907  pcfaclem  12912  pcfac  12913  pcbc  12914  expnprm  12916  oddprmdvds  12917  prmpwdvds  12918  pockthlem  12919  pockthg  12920  pockthi  12921  1arith  12930  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  4sqlem19  12972  znidom  14661  wilthlem1  15694  dvdsppwf1o  15703  sgmppw  15706  0sgmppw  15707  1sgmprm  15708  mersenne  15711  perfect1  15712  perfect  15715  lgslem1  15719  lgslem4  15722  lgsval  15723  lgsval2lem  15729  lgsvalmod  15738  lgsmod  15745  lgsdirprm  15753  lgsne0  15757  lgsprme0  15761  gausslemma2dlem0c  15770  gausslemma2dlem1a  15777  gausslemma2dlem5a  15784  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem3  15798  lgsquad2lem2  15801  lgsquad2  15802  m1lgs  15804  2lgslem1a  15807  2lgslem1c  15809  2lgs  15823  2sqlem3  15836  2sqlem8  15842