Theorem 0nn0 9582

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 2238	. 2 |- 0 = 0
2		elnn0 9569	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 133	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 748	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

This proof depends on syntax axioms:   \/ wo 720   = wceq 1402   e. wcel 2209   0cc0 8179   NNcn 9306   NN0cn0 9567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-n0 9568

This theorem is used by:  0xnn0  9640  elnn0z  9661  nn0ind-raph  9767  10nn0  9802  declei  9821  numlti  9822  nummul1c  9834  decaddc2  9841  decrmanc  9842  decrmac  9843  decaddm10  9844  decaddi  9845  decaddci  9846  decaddci2  9847  decmul1  9849  decmulnc  9852  6p5e11  9858  7p4e11  9861  8p3e11  9866  9p2e11  9872  10p10e20  9880  fz01or  10528  0elfz  10535  4fvwrd4  10557  fvinim0ffz  10670  0tonninf  10890  exple1  11045  sq10  11164  bc0k  11208  bcn1  11210  bccl  11219  fihasheq0  11246  hashfibc  11297  iswrdiz  11325  iswrddm0  11342  s1leng  11406  s1fv  11408  eqs1  11410  s111  11413  ccat2s1fstg  11430  pfx00g  11461  s2fv0g  11573  s3fv0g  11577  fsumnn0cl  12186  binom  12267  bcxmas  12272  isumnn0nn  12276  geoserap  12290  ef0lem  12443  ege2le3  12454  ef4p  12477  efgt1p2  12478  efgt1p  12479  nn0o  12690  ndvdssub  12713  5ndvds3  12717  bits0  12731  0bits  12742  gcdval  12752  gcdcl  12759  dfgcd3  12803  nn0seqcvgd  12835  algcvg  12842  eucalg  12853  lcmcl  12866  pwbdvdslemn  12960  pclem0  13085  pcpre1  13091  pcfac  13149  dec5dvds2  13212  2exp11  13236  2exp16  13237  10nprm  13248  11prm  13249  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  ennnfonelemj0  13341  ennnfonelem0  13345  ennnfonelem1  13347  plendxnocndx  13617  slotsdifdsndx  13628  slotsdifunifndx  13635  imasvalstrd  13668  gsum0cmn  14203  cnfldstr  14944  nn0subm  14969  znf1o  15035  fczpsrbag  15105  psr1clfi  15128  mplsubgfilemm  15138  dveflem  15876  plyconst  15895  plycolemc  15908  pilem3  15934  log2ublem3  16142  log2ublog2  16143  ppiublem2  16193  bclbnd  16205  clwwlkn0  16747  clwwlk0on0  16770  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  konigsberg  16832  1kp2ke3k  16836  ex-fac  16840  depindlem1  16845  012of  17121  isomninnlem  17177  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200