Theorem prmnn 12700

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

Syntax hints:   → wi 4   ∈ wcel 2202  {crab 2514   class class class wbr 4088  2_oc2o 6576   ≈ cen 6907  ℕcn 9143   ∥ cdvds 12366  ℙcprime 12697

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 12698

This theorem is referenced by:  prmz  12701  prmssnn  12702  nprmdvds1  12730  isprm5lem  12731  isprm5  12732  coprm  12734  euclemma  12736  prmdvdsexpr  12740  cncongrprm  12747  phiprmpw  12812  fermltl  12824  prmdiv  12825  prmdiveq  12826  prmdivdiv  12827  m1dvdsndvds  12839  vfermltl  12842  powm2modprm  12843  reumodprminv  12844  modprm0  12845  nnnn0modprm0  12846  modprmn0modprm0  12847  oddprm  12850  nnoddn2prm  12851  prm23lt5  12854  pcpremul  12884  pcdvdsb  12911  pcelnn  12912  pcidlem  12914  pcid  12915  pcdvdstr  12918  pcgcd1  12919  pcprmpw2  12924  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  pcaddlem  12930  pcadd  12931  pcmptcl  12933  pcmpt  12934  pcmpt2  12935  pcfaclem  12940  pcfac  12941  pcbc  12942  expnprm  12944  oddprmdvds  12945  prmpwdvds  12946  pockthlem  12947  pockthg  12948  pockthi  12949  1arith  12958  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  4sqlem19  13000  znidom  14690  wilthlem1  15723  dvdsppwf1o  15732  sgmppw  15735  0sgmppw  15736  1sgmprm  15737  mersenne  15740  perfect1  15741  perfect  15744  lgslem1  15748  lgslem4  15751  lgsval  15752  lgsval2lem  15758  lgsvalmod  15767  lgsmod  15774  lgsdirprm  15782  lgsne0  15786  lgsprme0  15790  gausslemma2dlem0c  15799  gausslemma2dlem1a  15806  gausslemma2dlem5a  15813  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem3  15827  lgsquad2lem2  15830  lgsquad2  15831  m1lgs  15833  2lgslem1a  15836  2lgslem1c  15838  2lgs  15852  2sqlem3  15865  2sqlem8  15871