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

Theorem 0nn0 9859
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0  |-  0  e.  NN0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2253 . 2  |-  0  =  0
2 elnn0 9846 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 199 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 386 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 10 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 359    = wceq 1619    e. wcel 1621   0cc0 8617   NNcn 9626   NN0cn0 9844
This theorem is referenced by:  nn0ind-raph  9991  numlti  10027  nummul1c  10039  decaddc2  10046  decaddi  10047  decaddci  10048  decaddci2  10049  6p5e11  10053  7p4e11  10055  8p3e11  10059  9p2e11  10065  10p10e20  10073  exple1  11039  nn0opth2  11165  faclbnd4lem3  11186  bcn1  11203  bccl  11212  hasheq0  11231  hashbc  11268  iswrdi  11294  s1cl  11318  s1fv  11323  splfv2a  11348  wrdeqs1cat  11352  s2fv0  11412  s3fv0  11415  fsumnn0cl  12086  binom  12165  bcxmas  12171  isumnn0nn  12175  climcndslem1  12182  geoser  12199  geomulcvg  12206  ef0lem  12234  ege2le3  12245  ef4p  12267  efgt1p2  12268  efgt1p  12269  ruclem11  12392  nthruz  12404  ndvdssub  12480  bits0  12493  0bits  12504  sadcf  12518  sadc0  12519  sadcaddlem  12522  sadcadd  12523  sadadd2lem  12524  sadadd2  12525  smupf  12543  smup0  12544  smumullem  12557  gcdcl  12570  nn0seqcvgd  12614  algcvg  12620  eucalg  12631  pclem  12765  pcfac  12821  vdwap0  12897  vdwap1  12898  vdwlem6  12907  hashbc0  12926  0hashbc  12928  0ram  12941  0ramcl  12944  ramz2  12945  ramz  12946  ramcl  12950  dec5dvds2  12954  2exp16  12977  11prm  12990  37prm  12996  43prm  12997  83prm  12998  139prm  12999  163prm  13000  317prm  13001  631prm  13002  1259lem1  13003  1259lem2  13004  1259lem3  13005  1259lem4  13006  1259lem5  13007  2503lem1  13009  2503lem2  13010  2503lem3  13011  2503prm  13012  4001lem1  13013  4001lem2  13014  4001lem3  13015  4001lem4  13016  4001prm  13017  odrngstr  13185  imasvalstr  13226  ipostr  14100  gsumws1  14297  oddvdsnn0  14694  pgp0  14742  sylow1lem1  14744  cyggex2  15018  psrbas  15956  psrlidm  15980  psrridm  15981  mvridlem  15996  mvrf1  16002  mplcoe3  16042  mplcoe2  16043  ltbwe  16046  psrbag0  16067  psrbagsn  16068  00ply1bas  16150  ply1plusgfvi  16152  coe1sclmul  16190  coe1sclmul2  16192  coe1scl  16194  ply1sclid  16195  cnfldstr  16211  nn0subm  16259  expmhm  16281  znf1o  16337  zzngim  16338  cygznlem1  16352  cygznlem2a  16353  cygznlem3  16355  cygth  16357  thlle  16429  dscmet  17927  itgcnlem  18976  dvn0  19105  dvn1  19107  cpncn  19117  dveflem  19158  c1lip2  19177  evlslem1  19231  tdeglem4  19278  deg1le0  19329  ply1divex  19354  ply1rem  19381  fta1g  19385  plyconst  19420  plypf1  19426  plyco  19455  0dgr  19459  0dgrb  19460  coefv0  19461  dgreq0  19478  vieta1lem2  19523  vieta1  19524  aareccl  19538  aannenlem2  19541  taylthlem1  19584  radcnv0  19624  abelthlem6  19644  abelthlem9  19648  logtayl  19839  cxp0  19885  cxpeq  19965  leibpilem2  20069  leibpi  20070  log2ublem3  20076  log2ub  20077  birthday  20081  divsqrsumlem  20106  sqff1o  20252  ppiublem2  20274  chtublem  20282  bclbnd  20351  bpos1  20354  bposlem8  20362  lgsval  20371  dchrisum0flblem1  20489  dchrisum0flb  20491  ostth2lem2  20615  1kp2ke3k  20646  subfac0  22879  subfacval2  22889  subfaclim  22890  cvmliftlem7  22993  cvmliftlem13  22998  eupa0  23069  konigsberg  23082  relexp0  23196  relexp1  23198  rtrclreclem.refl  23212  bpoly0  23959  bpoly2  23966  bpoly3  23967  bpoly4  23968  fsumcube  23969  empklst  25175  heiborlem4  25704  heiborlem10  25710  nacsfix  25953  diophrw  26004  pell1qr1  26122  monotoddzzfi  26193  jm2.23  26255  hbtlem5  26498  mncn0  26510  aaitgo  26533  psgnunilem2  26584  psgnunilem3  26585  mon1pid  26690
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-mulcl 8679  ax-i2m1 8685
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-sn 3550  df-n0 9845
  Copyright terms: Public domain W3C validator