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

Theorem 0nn0 11184
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0 0 ∈ ℕ0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2610 . 2 0 = 0
2 elnn0 11171 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 217 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 409 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 5 1 0 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wo 382   = wceq 1475  wcel 1977  0cc0 9815  cn 10897  0cn0 11169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-n0 11170
This theorem is referenced by:  0xnn0  11246  nn0ind-raph  11353  10nn0  11392  declei  11418  numlti  11421  nummul1c  11438  decaddc2OLD  11450  decaddc2  11451  decrmanc  11452  decrmac  11453  decaddm10  11454  decaddi  11455  decaddci  11456  decaddci2  11457  decaddci2OLD  11458  decmul1  11461  decmul1OLD  11462  decmulnc  11467  6p5e11  11476  6p5e11OLD  11477  7p4e11  11481  7p4e11OLD  11482  8p3e11  11488  8p3e11OLD  11489  9p2e11  11495  9p2e11OLD  11496  10p10e20  11504  10p10e20OLD  11505  xnn0n0n1ge2b  11841  0elfz  12305  4fvwrd4  12328  fvinim0ffz  12449  ssnn0fi  12646  fsuppmapnn0fiubex  12654  exple1  12782  sq10  12910  nn0opth2  12921  faclbnd4lem3  12944  bc0k  12960  bcn1  12962  bccl  12971  hasheq0  13015  hashrabrsn  13022  hashbc  13094  fi1uzind  13134  brfi1ind  13136  opfi1ind  13139  fi1uzindOLD  13140  brfi1indOLD  13142  opfi1indOLD  13145  iswrdi  13164  s1fv  13243  ccat2s1fst  13268  2swrdeqwrdeq  13305  wrdeqs1cat  13326  splfv2a  13358  repsw0  13375  0csh0  13390  repswcshw  13409  cshw1  13419  s2fv0  13482  s3fv0  13486  s4fv0  13490  ofs1  13557  relexp0g  13610  relexpaddg  13641  rtrclreclem1  13646  fsumnn0cl  14314  binom  14401  bcxmas  14406  isumnn0nn  14413  climcndslem1  14420  geoser  14438  geomulcvg  14446  risefac0  14597  fallfac0  14598  risefac1  14603  fallfac1  14604  binomfallfaclem2  14610  binomfallfac  14611  bpoly0  14620  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  ef0lem  14648  ege2le3  14659  ef4p  14682  efgt1p2  14683  efgt1p  14684  ruclem11  14808  nthruz  14820  nn0o  14937  ndvdssub  14971  bits0  14988  0bits  14999  sadcf  15013  sadc0  15014  sadcaddlem  15017  sadcadd  15018  sadadd2lem  15019  sadadd2  15020  smupf  15038  smup0  15039  smumullem  15052  gcdcl  15066  nn0seqcvgd  15121  algcvg  15127  eucalg  15138  lcmcl  15152  lcmfval  15172  lcmfcl  15179  pclem  15381  pcfac  15441  vdwap0  15518  vdwap1  15519  vdwlem6  15528  hashbc0  15547  0ram  15562  0ramcl  15565  ramz2  15566  ramz  15567  ramcl  15571  prmo0  15578  dec5dvds2  15607  2exp16  15635  11prm  15660  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  odrngstr  15889  imasvalstr  15935  ipostr  16976  gsumws1  17199  psgnunilem2  17738  psgnunilem3  17739  oddvdsnn0  17786  pgp0  17834  sylow1lem1  17836  cyggex2  18121  telgsums  18213  srgbinomlem3  18365  srgbinomlem4  18366  srgbinom  18368  snifpsrbag  19187  fczpsrbag  19188  psrlidm  19224  mvrf1  19246  mplcoe3  19287  mplcoe5  19289  ltbwe  19293  psrbag0  19315  psrbagsn  19316  evlslem1  19336  00ply1bas  19431  ply1plusgfvi  19433  coe1sclmul  19473  coe1sclmul2  19475  coe1scl  19478  ply1sclid  19479  ply1idvr1  19484  cply1coe0bi  19491  cnfldstr  19569  nn0subm  19620  expmhm  19634  nn0srg  19635  znf1o  19719  zzngim  19720  cygznlem1  19734  cygznlem2a  19735  cygznlem3  19737  cygth  19739  thlle  19860  cpm2mf  20376  m2cpminvid2lem  20378  m2cpminvid2  20379  m2cpmfo  20380  decpmatid  20394  pmatcollpw3  20408  pmatcollpw3fi1lem1  20410  pmatcollpwscmatlem1  20413  pmatcollpwscmatlem2  20414  idpm2idmp  20425  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cpmadugsumlemF  20500  dscmet  22187  itgcnlem  23362  dvn0  23493  dvn1  23495  cpncn  23505  dveflem  23546  c1lip2  23565  tdeglem4  23624  deg1le0  23675  ply1divex  23700  ply1rem  23727  fta1g  23731  plyconst  23766  plypf1  23772  plyco  23801  0dgr  23805  0dgrb  23806  coefv0  23808  dgreq0  23825  vieta1lem2  23870  vieta1  23871  aareccl  23885  aannenlem2  23888  taylthlem1  23931  radcnv0  23974  abelthlem6  23994  abelthlem9  23998  logtayl  24206  cxp0  24216  cxpeq  24298  leibpilem2  24468  leibpi  24469  log2ublem3  24475  log2ub  24476  log2le1  24477  birthday  24481  divsqrtsumlem  24506  dmgmn0  24552  lgambdd  24563  sqff1o  24708  ppiublem2  24728  chtublem  24736  bclbnd  24805  bposlem8  24816  lgsval  24826  dchrisum0flblem1  24997  dchrisum0flb  24999  ostth2lem2  25123  usgraex0elv  25924  usgrafisbase  25943  wlkonwlk  26065  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv  26195  wwlkn0  26217  wwlkn0s  26233  clwwlkn0  26302  clwwlkf1  26324  erclwwlkref  26341  0egra0rgra  26463  rusgranumwlkb0  26480  rusgra0edg  26482  eupa0  26501  1kp2ke3k  26695  ex-fac  26700  ex-prmo  26708  nn0min  28954  lmatcl  29210  lmat22e12  29213  lmat22e21  29214  fsumcvg4  29324  oddpwdc  29743  eulerpartlems  29749  eulerpartlemb  29757  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  fib0  29788  fib1  29789  fibp1  29790  ofcs1  29947  signsply0  29954  signsvvf  29982  subfac0  30413  subfacval2  30423  subfaclim  30424  cvmliftlem7  30527  cvmliftlem13  30532  bccolsum  30878  fwddifn0  31441  heiborlem4  32783  heiborlem10  32789  nacsfix  36293  diophrw  36340  pell1qr1  36453  monotoddzzfi  36525  jm2.23  36581  hbtlem5  36717  mncn0  36728  aaitgo  36751  mon1pid  36802  brfvrcld  37002  corclrcl  37018  dfrtrcl3  37044  fvrtrcllb0d  37046  fvrtrcllb0da  37047  corcltrcl  37050  cotrclrcl  37053  k0004val0  37472  bccn0  37564  bccn1  37565  binomcxplemradcnv  37573  binomcxplemnotnn0  37577  dvnmul  38833  dvnprodlem3  38838  wallispilem2  38959  wallispi2lem2  38965  stirlinglem5  38971  stirlinglem7  38973  fourierdlem83  39082  fourierdlem112  39111  fouriersw  39124  elaa2lem  39126  elaa2  39127  etransclem48  39175  etransc  39176  iccelpart  39971  fmtno0  39990  fmtnorec2  39993  fmtno5lem1  40003  fmtno5lem2  40004  fmtno5lem4  40006  257prm  40011  fmtnofac2  40019  fmtnofac1  40020  fmtno4prmfac  40022  fmtno4nprmfac193  40024  fmtno5faclem1  40029  fmtno5faclem2  40030  fmtno5faclem3  40031  fmtno5fac  40032  fmtno5nprm  40033  139prmALT  40049  31prm  40050  127prm  40053  2exp11  40055  m11nprm  40056  bits0ALTV  40128  evengpoap3  40215  tgoldbachlt  40230  tgoldbach  40232  tgoldbachltOLD  40237  tgoldbachOLD  40239  pfx2  40275  usgr0edg0rusgr  40775  usgr2pthlem  40969  wwlksn0s  41057  rusgrnumwwlkb0  41174  clwwlksf1  41224  erclwwlksref  41241  0wlkOnlem1  41286  upgr4cycl4dv4e  41352  ssnn0ssfz  41920  dig1  42200  0dig2nn0e  42204  0dig2nn0o  42205
  Copyright terms: Public domain W3C validator