Theorem 0nn0 10586

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	|- 0 e. NN0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2437	. 2 |- 0 = 0
2		elnn0 10573	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 206	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 395	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 368   = wceq 1369   e. wcel 1756   0cc0 9274   NNcn 10314   NN0cn0 10571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-i2m1 9342

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-un 3326  df-sn 3871  df-n0 10572

This theorem is referenced by:  nn0ind-raph  10734  numlti  10771  nummul1c  10783  decaddc2  10790  decaddi  10791  decaddci  10792  decaddci2  10793  6p5e11  10797  7p4e11  10799  8p3e11  10803  9p2e11  10809  10p10e20  10817  0elfz  11475  4fvwrd4  11525  injresinjlem  11630  exple1  11915  nn0opth2  12042  faclbnd4lem3  12063  bc0k  12079  bcn1  12081  bccl  12090  hasheq0  12123  hashrabrsn  12129  hashbc  12198  brfi1uzind  12211  brfi1ind  12212  iswrdi  12231  s1fv  12290  2swrdeqwrdeq  12339  wrdeqs1cat  12361  splfv2a  12390  repsw0  12407  0csh0  12422  repswcshw  12438  cshw1  12448  s2fv0  12504  s3fv0  12507  fsumnn0cl  13205  binom  13285  bcxmas  13290  isumnn0nn  13297  climcndslem1  13304  geoser  13321  geomulcvg  13328  ef0lem  13356  ege2le3  13367  ef4p  13389  efgt1p2  13390  efgt1p  13391  ruclem11  13514  nthruz  13526  ndvdssub  13603  bits0  13616  0bits  13627  sadcf  13641  sadc0  13642  sadcaddlem  13645  sadcadd  13646  sadadd2lem  13647  sadadd2  13648  smupf  13666  smup0  13667  smumullem  13680  gcdcl  13693  nn0seqcvgd  13737  algcvg  13743  eucalg  13754  pclem  13897  pcfac  13953  vdwap0  14029  vdwap1  14030  vdwlem6  14039  hashbc0  14058  0ram  14073  0ramcl  14076  ramz2  14077  ramz  14078  ramcl  14082  dec5dvds2  14086  2exp16  14109  11prm  14134  37prm  14140  43prm  14141  83prm  14142  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  odrngstr  14337  imasvalstr  14382  ipostr  15315  gsumws1  15506  psgnunilem2  15990  psgnunilem3  15991  oddvdsnn0  16036  pgp0  16084  sylow1lem1  16086  cyggex2  16362  srgbinomlem3  16626  srgbinomlem4  16627  srgbinom  16629  snifpsrbag  17407  fczpsrbag  17408  psrbasOLD  17423  psrlidm  17448  psrlidmOLD  17449  psrridmOLD  17451  mvridlemOLD  17466  mvrf1  17472  mplcoe3  17519  mplcoe3OLD  17520  mplcoe2  17521  mplcoe2OLD  17522  ltbwe  17526  psrbag0  17548  psrbagsn  17549  evlslem1  17573  00ply1bas  17666  ply1plusgfvi  17668  coe1sclmul  17706  coe1sclmul2  17708  coe1scl  17710  ply1sclid  17711  cnfldstr  17789  nn0subm  17837  expmhm  17849  nn0srg  17850  znf1o  17953  zzngim  17954  cygznlem1  17968  cygznlem2a  17969  cygznlem3  17971  cygth  17973  thlle  18091  dscmet  20134  itgcnlem  21236  dvn0  21367  dvn1  21369  cpncn  21379  dveflem  21420  c1lip2  21439  tdeglem4  21498  deg1le0  21552  ply1divex  21577  ply1rem  21604  fta1g  21608  plyconst  21643  plypf1  21649  plyco  21678  0dgr  21682  0dgrb  21683  coefv0  21684  dgreq0  21701  vieta1lem2  21746  vieta1  21747  aareccl  21761  aannenlem2  21764  taylthlem1  21807  radcnv0  21850  abelthlem6  21870  abelthlem9  21874  logtayl  22074  cxp0  22084  cxpeq  22164  leibpilem2  22305  leibpi  22306  log2ublem3  22312  log2ub  22313  birthday  22317  divsqrsumlem  22342  sqff1o  22489  ppiublem2  22511  chtublem  22519  bclbnd  22588  bpos1  22591  bposlem8  22599  lgsval  22608  dchrisum0flblem1  22726  dchrisum0flb  22728  ostth2lem2  22852  usgraex0elv  23259  usgrafisbase  23272  wlkonwlk  23379  cyclnspth  23462  cyclispthon  23464  3v3e3cycl1  23475  4cycl4v4e  23497  4cycl4dv  23498  eupa0  23540  konigsberg  23553  1kp2ke3k  23598  nn0min  26035  fsumcvg4  26328  nexple  26396  log2le1  26414  oddpwdc  26685  eulerpartlems  26691  eulerpartlemb  26699  eulerpartlemt  26702  eulerpartgbij  26703  eulerpartlemmf  26706  eulerpartlemgf  26710  eulerpartlemgs2  26711  eulerpartlemn  26712  fib0  26730  fib1  26731  fibp1  26732  ofs1  26891  ofcs1  26892  signsply0  26900  signsvvf  26928  dmgmn0  26960  lgambdd  26971  subfac0  27013  subfacval2  27023  subfaclim  27024  cvmliftlem7  27128  cvmliftlem13  27133  relexp0  27278  relexp1  27280  rtrclreclem.refl  27293  risefac0  27477  fallfac0  27478  risefac1  27483  fallfac1  27484  binomfallfaclem2  27490  binomfallfac  27491  bpoly0  28140  bpoly2  28147  bpoly3  28148  bpoly4  28149  fsumcube  28150  heiborlem4  28656  heiborlem10  28662  nacsfix  28991  diophrw  29040  pell1qr1  29155  monotoddzzfi  29226  jm2.23  29288  hbtlem5  29427  mncn0  29439  aaitgo  29462  mon1pid  29516  wallispilem2  29804  wallispi2lem2  29810  stirlinglem5  29816  stirlinglem7  29818  ccat2s1fst  30215  usgra2pthlem1  30243  wwlkn0  30266  wwlkn0s  30282  clwwlkn0  30380  clwwlkf1  30401  erclwwlkref  30426  0egra0rgra  30492  rusgranumwlkb0  30514  rusgra0edg  30516  ply1idvr1  30746