Theorem 0nn0 9395

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 2229	. 2 |- 0 = 0
2		elnn0 9382	. . . 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 741	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 713   = wceq 1395   e. wcel 2200   0cc0 8010   NNcn 9121   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9381

This theorem is referenced by:  0xnn0  9449  elnn0z  9470  nn0ind-raph  9575  10nn0  9606  declei  9624  numlti  9625  nummul1c  9637  decaddc2  9644  decrmanc  9645  decrmac  9646  decaddm10  9647  decaddi  9648  decaddci  9649  decaddci2  9650  decmul1  9652  decmulnc  9655  6p5e11  9661  7p4e11  9664  8p3e11  9669  9p2e11  9675  10p10e20  9683  fz01or  10319  0elfz  10326  4fvwrd4  10348  fvinim0ffz  10459  0tonninf  10674  exple1  10829  sq10  10946  bc0k  10990  bcn1  10992  bccl  11001  fihasheq0  11027  iswrdiz  11091  iswrddm0  11108  s1leng  11172  s1fv  11174  eqs1  11176  s111  11179  pfx00g  11223  s2fv0g  11335  s3fv0g  11339  fsumnn0cl  11930  binom  12011  bcxmas  12016  isumnn0nn  12020  geoserap  12034  ef0lem  12187  ege2le3  12198  ef4p  12221  efgt1p2  12222  efgt1p  12223  nn0o  12434  ndvdssub  12457  5ndvds3  12461  bits0  12475  0bits  12486  gcdval  12496  gcdcl  12503  dfgcd3  12547  nn0seqcvgd  12579  algcvg  12586  eucalg  12597  lcmcl  12610  pw2dvdslemn  12703  pclem0  12825  pcpre1  12831  pcfac  12889  dec5dvds2  12952  2exp11  12975  2exp16  12976  ennnfonelemj0  12988  ennnfonelem0  12992  ennnfonelem1  12994  plendxnocndx  13263  slotsdifdsndx  13274  slotsdifunifndx  13281  imasvalstrd  13319  cnfldstr  14538  nn0subm  14563  znf1o  14631  fczpsrbag  14651  psr1clfi  14668  mplsubgfilemm  14678  dveflem  15416  plyconst  15435  plycolemc  15448  pilem3  15473  clwwlkn0  16151  1kp2ke3k  16171  ex-fac  16175  012of  16444  isomninnlem  16486  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508