MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmnn Structured version   Visualization version   GIF version

Theorem prmnn 15435
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 15434 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2𝑜))
21simplbi 475 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  {crab 2945   class class class wbr 4685  2𝑜c2o 7599  cen 7994  cn 11058  cdvds 15027  cprime 15432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-prm 15433
This theorem is referenced by:  prmz  15436  prmssnn  15437  nprmdvds1  15465  isprm5  15466  coprm  15470  prmdvdsexpr  15476  prmndvdsfaclt  15482  cncongrprm  15484  phiprmpw  15528  fermltl  15536  prmdiv  15537  prmdiveq  15538  prmdivdiv  15539  modprm1div  15549  m1dvdsndvds  15550  vfermltl  15553  vfermltlALT  15554  powm2modprm  15555  reumodprminv  15556  modprm0  15557  nnnn0modprm0  15558  modprmn0modprm0  15559  oddprm  15562  nnoddn2prm  15563  prm23lt5  15566  pcpremul  15595  pcdvdsb  15620  pcelnn  15621  pcidlem  15623  pcid  15624  pcdvdstr  15627  pcgcd1  15628  pcprmpw2  15633  dvdsprmpweqnn  15636  dvdsprmpweqle  15637  pcaddlem  15639  pcadd  15640  pcmptcl  15642  pcmpt  15643  pcmpt2  15644  pcfaclem  15649  pcfac  15650  pcbc  15651  expnprm  15653  oddprmdvds  15654  prmpwdvds  15655  pockthlem  15656  pockthg  15657  pockthi  15658  prminf  15666  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  prmrec  15673  1arith  15678  4sqlem11  15706  4sqlem12  15707  4sqlem13  15708  4sqlem14  15709  4sqlem17  15712  4sqlem18  15713  4sqlem19  15714  prmdvdsprmo  15793  prmgaplem3  15804  prmgaplem4  15805  prmgaplem5  15806  prmgaplem6  15807  prmgaplem8  15809  cshwshashnsame  15857  cshwshash  15858  prmlem1a  15860  pgpfi1  18056  pgp0  18057  sylow1lem1  18059  sylow1lem3  18061  sylow1lem4  18062  sylow1lem5  18063  odcau  18065  pgpfi  18066  fislw  18086  sylow3lem6  18093  gexexlem  18301  prmcyg  18341  ablfac1lem  18513  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem3a  18521  pgpfac1lem3  18522  ablfaclem3  18532  prmirredlem  19889  dfprm2  19890  prmirred  19891  znfld  19957  wilthlem1  24839  wilthlem2  24840  wilthlem3  24841  prmdvdsfi  24878  chtf  24879  efchtcl  24882  vmaval  24884  isppw2  24886  vmappw  24887  vmaprm  24888  vmacl  24889  efvmacl  24891  muval1  24904  chtprm  24924  chtdif  24929  efchtdvds  24930  mumul  24952  sqff1o  24953  dvdsppwf1o  24957  sgmppw  24967  0sgmppw  24968  1sgmprm  24969  vmalelog  24975  chtleppi  24980  chtublem  24981  fsumvma2  24984  vmasum  24986  chpchtsum  24989  chpub  24990  mersenne  24997  perfect1  24998  perfect  25001  pcbcctr  25046  bpos1lem  25052  bposlem1  25054  bposlem2  25055  bposlem6  25059  lgslem1  25067  lgsval2lem  25077  lgsvalmod  25086  lgsmod  25093  lgsdirprm  25101  lgsne0  25105  lgsprme0  25109  lgsqrlem1  25116  lgsqrlem2  25117  lgsqrlem4  25119  lgsqr  25121  lgsqrmod  25122  lgsqrmodndvds  25123  gausslemma2dlem0c  25128  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  gausslemma2dlem5a  25140  gausslemma2dlem7  25143  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad2lem2  25155  lgsquad2  25156  m1lgs  25158  2lgslem1a  25161  2lgslem1c  25163  2lgs  25177  2sqlem3  25190  2sqlem8  25196  2sqlem11  25199  2sqblem  25201  chtppilimlem1  25207  rplogsumlem2  25219  rpvmasumlem  25221  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dirith2  25262  padicabvf  25365  ostth1  25367  ostth3  25372  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  fusgrhashclwwlkn  27043  clwlksfclwwlk  27049  clwlksfoclwwlk  27050  clwlksf1clwwlk  27056  numclwwlk5  27375  numclwwlk6  27377  numclwwlk7  27378  numclwwlk8  27379  2sqmod  29776  nn0prpwlem  32442  nn0prpw  32443  nzprmdif  38835  etransclem41  40810  etransclem44  40813  etransclem47  40816  etransclem48  40817  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnoprmfac1  41802  fmtnoprmfac2  41804  prmdvdsfmtnof1lem2  41822  2pwp1prm  41828  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem3  41849  lighneallem4  41852  lighneal  41853  perfectALTV  41957  gbepos  41971  gbowpos  41972  sbgoldbaltlem1  41992  ztprmneprm  42450
  Copyright terms: Public domain W3C validator