ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prmnn GIF version

Theorem prmnn 12031
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.
StepHypRef Expression
1 isprm 12030 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2o))
21simplbi 272 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2135  {crab 2446   class class class wbr 3977  2oc2o 6370  cen 6696  cn 8849  cdvds 11717  cprime 12028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rab 2451  df-v 2724  df-un 3116  df-sn 3577  df-pr 3578  df-op 3580  df-br 3978  df-prm 12029
This theorem is referenced by:  prmz  12032  prmssnn  12033  nprmdvds1  12061  isprm5lem  12062  isprm5  12063  coprm  12065  euclemma  12067  prmdvdsexpr  12071  cncongrprm  12078  phiprmpw  12143  fermltl  12155  prmdiv  12156  prmdiveq  12157  prmdivdiv  12158  m1dvdsndvds  12169  vfermltl  12172  powm2modprm  12173  reumodprminv  12174  modprm0  12175  nnnn0modprm0  12176  modprmn0modprm0  12177  oddprm  12180  nnoddn2prm  12181  prm23lt5  12184  pcpremul  12214  pcdvdsb  12240  pcelnn  12241  pcidlem  12243  pcid  12244  pcdvdstr  12247  pcgcd1  12248  pcprmpw2  12253  dvdsprmpweqnn  12256  dvdsprmpweqle  12257  pcaddlem  12259  pcadd  12260  pcmptcl  12261  pcmpt  12262  pcmpt2  12263  pcfaclem  12268  pcfac  12269  pcbc  12270  expnprm  12272  oddprmdvds  12273  prmpwdvds  12274  pockthlem  12275  pockthg  12276  pockthi  12277  1arith  12286
  Copyright terms: Public domain W3C validator