Theorem prmnn 12627

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

Syntax hints:   → wi 4   ∈ wcel 2200  {crab 2512   class class class wbr 4082  2_oc2o 6554   ≈ cen 6883  ℕcn 9106   ∥ cdvds 12293  ℙcprime 12624

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-prm 12625

This theorem is referenced by:  prmz  12628  prmssnn  12629  nprmdvds1  12657  isprm5lem  12658  isprm5  12659  coprm  12661  euclemma  12663  prmdvdsexpr  12667  cncongrprm  12674  phiprmpw  12739  fermltl  12751  prmdiv  12752  prmdiveq  12753  prmdivdiv  12754  m1dvdsndvds  12766  vfermltl  12769  powm2modprm  12770  reumodprminv  12771  modprm0  12772  nnnn0modprm0  12773  modprmn0modprm0  12774  oddprm  12777  nnoddn2prm  12778  prm23lt5  12781  pcpremul  12811  pcdvdsb  12838  pcelnn  12839  pcidlem  12841  pcid  12842  pcdvdstr  12845  pcgcd1  12846  pcprmpw2  12851  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  pcaddlem  12857  pcadd  12858  pcmptcl  12860  pcmpt  12861  pcmpt2  12862  pcfaclem  12867  pcfac  12868  pcbc  12869  expnprm  12871  oddprmdvds  12872  prmpwdvds  12873  pockthlem  12874  pockthg  12875  pockthi  12876  1arith  12885  4sqlem11  12919  4sqlem12  12920  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  4sqlem19  12927  znidom  14615  wilthlem1  15648  dvdsppwf1o  15657  sgmppw  15660  0sgmppw  15661  1sgmprm  15662  mersenne  15665  perfect1  15666  perfect  15669  lgslem1  15673  lgslem4  15676  lgsval  15677  lgsval2lem  15683  lgsvalmod  15692  lgsmod  15699  lgsdirprm  15707  lgsne0  15711  lgsprme0  15715  gausslemma2dlem0c  15724  gausslemma2dlem1a  15731  gausslemma2dlem5a  15738  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem3  15752  lgsquad2lem2  15755  lgsquad2  15756  m1lgs  15758  2lgslem1a  15761  2lgslem1c  15763  2lgs  15777  2sqlem3  15790  2sqlem8  15796