Theorem 0nn0 9417

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 2231	. 2 |- 0 = 0
2		elnn0 9404	. . . 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 743	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 715   = wceq 1397   e. wcel 2202   0cc0 8032   NNcn 9143   NN0cn0 9402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-n0 9403

This theorem is referenced by:  0xnn0  9471  elnn0z  9492  nn0ind-raph  9597  10nn0  9628  declei  9646  numlti  9647  nummul1c  9659  decaddc2  9666  decrmanc  9667  decrmac  9668  decaddm10  9669  decaddi  9670  decaddci  9671  decaddci2  9672  decmul1  9674  decmulnc  9677  6p5e11  9683  7p4e11  9686  8p3e11  9691  9p2e11  9697  10p10e20  9705  fz01or  10346  0elfz  10353  4fvwrd4  10375  fvinim0ffz  10488  0tonninf  10703  exple1  10858  sq10  10975  bc0k  11019  bcn1  11021  bccl  11030  fihasheq0  11056  iswrdiz  11124  iswrddm0  11141  s1leng  11205  s1fv  11207  eqs1  11209  s111  11212  ccat2s1fstg  11229  pfx00g  11260  s2fv0g  11372  s3fv0g  11376  fsumnn0cl  11982  binom  12063  bcxmas  12068  isumnn0nn  12072  geoserap  12086  ef0lem  12239  ege2le3  12250  ef4p  12273  efgt1p2  12274  efgt1p  12275  nn0o  12486  ndvdssub  12509  5ndvds3  12513  bits0  12527  0bits  12538  gcdval  12548  gcdcl  12555  dfgcd3  12599  nn0seqcvgd  12631  algcvg  12638  eucalg  12649  lcmcl  12662  pw2dvdslemn  12755  pclem0  12877  pcpre1  12883  pcfac  12941  dec5dvds2  13004  2exp11  13027  2exp16  13028  ennnfonelemj0  13040  ennnfonelem0  13044  ennnfonelem1  13046  plendxnocndx  13315  slotsdifdsndx  13326  slotsdifunifndx  13333  imasvalstrd  13371  cnfldstr  14591  nn0subm  14616  znf1o  14684  fczpsrbag  14704  psr1clfi  14721  mplsubgfilemm  14731  dveflem  15469  plyconst  15488  plycolemc  15501  pilem3  15526  clwwlkn0  16278  clwwlk0on0  16301  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  konigsberg  16363  1kp2ke3k  16367  ex-fac  16371  depindlem1  16376  012of  16643  isomninnlem  16685  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  gfsum0  16734