Theorem prmnn 12745

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

Syntax hints:   → wi 4   ∈ wcel 2202  {crab 2515   class class class wbr 4093  2_oc2o 6619   ≈ cen 6950  ℕcn 9185   ∥ cdvds 12411  ℙcprime 12742

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-prm 12743

This theorem is referenced by:  prmz  12746  prmssnn  12747  nprmdvds1  12775  isprm5lem  12776  isprm5  12777  coprm  12779  euclemma  12781  prmdvdsexpr  12785  cncongrprm  12792  phiprmpw  12857  fermltl  12869  prmdiv  12870  prmdiveq  12871  prmdivdiv  12872  m1dvdsndvds  12884  vfermltl  12887  powm2modprm  12888  reumodprminv  12889  modprm0  12890  nnnn0modprm0  12891  modprmn0modprm0  12892  oddprm  12895  nnoddn2prm  12896  prm23lt5  12899  pcpremul  12929  pcdvdsb  12956  pcelnn  12957  pcidlem  12959  pcid  12960  pcdvdstr  12963  pcgcd1  12964  pcprmpw2  12969  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  pcaddlem  12975  pcadd  12976  pcmptcl  12978  pcmpt  12979  pcmpt2  12980  pcfaclem  12985  pcfac  12986  pcbc  12987  expnprm  12989  oddprmdvds  12990  prmpwdvds  12991  pockthlem  12992  pockthg  12993  pockthi  12994  1arith  13003  4sqlem11  13037  4sqlem12  13038  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  4sqlem19  13045  znidom  14736  wilthlem1  15777  dvdsppwf1o  15786  sgmppw  15789  0sgmppw  15790  1sgmprm  15791  mersenne  15794  perfect1  15795  perfect  15798  lgslem1  15802  lgslem4  15805  lgsval  15806  lgsval2lem  15812  lgsvalmod  15821  lgsmod  15828  lgsdirprm  15836  lgsne0  15840  lgsprme0  15844  gausslemma2dlem0c  15853  gausslemma2dlem1a  15860  gausslemma2dlem5a  15867  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem3  15881  lgsquad2lem2  15884  lgsquad2  15885  m1lgs  15887  2lgslem1a  15890  2lgslem1c  15892  2lgs  15906  2sqlem3  15919  2sqlem8  15925