Theorem prmnn 12507

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

Syntax hints:   → wi 4   ∈ wcel 2177  {crab 2489   class class class wbr 4051  2_oc2o 6509   ≈ cen 6838  ℕcn 9056   ∥ cdvds 12173  ℙcprime 12504

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rab 2494  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-prm 12505

This theorem is referenced by:  prmz  12508  prmssnn  12509  nprmdvds1  12537  isprm5lem  12538  isprm5  12539  coprm  12541  euclemma  12543  prmdvdsexpr  12547  cncongrprm  12554  phiprmpw  12619  fermltl  12631  prmdiv  12632  prmdiveq  12633  prmdivdiv  12634  m1dvdsndvds  12646  vfermltl  12649  powm2modprm  12650  reumodprminv  12651  modprm0  12652  nnnn0modprm0  12653  modprmn0modprm0  12654  oddprm  12657  nnoddn2prm  12658  prm23lt5  12661  pcpremul  12691  pcdvdsb  12718  pcelnn  12719  pcidlem  12721  pcid  12722  pcdvdstr  12725  pcgcd1  12726  pcprmpw2  12731  dvdsprmpweqnn  12734  dvdsprmpweqle  12735  pcaddlem  12737  pcadd  12738  pcmptcl  12740  pcmpt  12741  pcmpt2  12742  pcfaclem  12747  pcfac  12748  pcbc  12749  expnprm  12751  oddprmdvds  12752  prmpwdvds  12753  pockthlem  12754  pockthg  12755  pockthi  12756  1arith  12765  4sqlem11  12799  4sqlem12  12800  4sqlem13m  12801  4sqlem14  12802  4sqlem17  12805  4sqlem18  12806  4sqlem19  12807  znidom  14494  wilthlem1  15527  dvdsppwf1o  15536  sgmppw  15539  0sgmppw  15540  1sgmprm  15541  mersenne  15544  perfect1  15545  perfect  15548  lgslem1  15552  lgslem4  15555  lgsval  15556  lgsval2lem  15562  lgsvalmod  15571  lgsmod  15578  lgsdirprm  15586  lgsne0  15590  lgsprme0  15594  gausslemma2dlem0c  15603  gausslemma2dlem1a  15610  gausslemma2dlem5a  15617  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  lgsquadlem1  15629  lgsquadlem3  15631  lgsquad2lem2  15634  lgsquad2  15635  m1lgs  15637  2lgslem1a  15640  2lgslem1c  15642  2lgs  15656  2sqlem3  15669  2sqlem8  15675