Theorem 0nn0 9578

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 9565	. . . 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 9304   NN0cn0 9563

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 9564

This theorem is used by:  0xnn0  9636  elnn0z  9657  nn0ind-raph  9763  10nn0  9794  declei  9812  numlti  9813  nummul1c  9825  decaddc2  9832  decrmanc  9833  decrmac  9834  decaddm10  9835  decaddi  9836  decaddci  9837  decaddci2  9838  decmul1  9840  decmulnc  9843  6p5e11  9849  7p4e11  9852  8p3e11  9857  9p2e11  9863  10p10e20  9871  fz01or  10518  0elfz  10525  4fvwrd4  10547  fvinim0ffz  10660  0tonninf  10877  exple1  11032  sq10  11150  bc0k  11194  bcn1  11196  bccl  11205  fihasheq0  11232  hashfibc  11283  iswrdiz  11311  iswrddm0  11328  s1leng  11392  s1fv  11394  eqs1  11396  s111  11399  ccat2s1fstg  11416  pfx00g  11447  s2fv0g  11559  s3fv0g  11563  fsumnn0cl  12170  binom  12251  bcxmas  12256  isumnn0nn  12260  geoserap  12274  ef0lem  12427  ege2le3  12438  ef4p  12461  efgt1p2  12462  efgt1p  12463  nn0o  12674  ndvdssub  12697  5ndvds3  12701  bits0  12715  0bits  12726  gcdval  12736  gcdcl  12743  dfgcd3  12787  nn0seqcvgd  12819  algcvg  12826  eucalg  12837  lcmcl  12850  pw2dvdslemn  12943  pclem0  13065  pcpre1  13071  pcfac  13129  dec5dvds2  13192  2exp11  13215  2exp16  13216  ennnfonelemj0  13292  ennnfonelem0  13296  ennnfonelem1  13298  plendxnocndx  13568  slotsdifdsndx  13579  slotsdifunifndx  13586  imasvalstrd  13619  gsum0cmn  14154  cnfldstr  14895  nn0subm  14920  znf1o  14986  fczpsrbag  15056  psr1clfi  15079  mplsubgfilemm  15089  dveflem  15827  plyconst  15846  plycolemc  15859  pilem3  15884  log2ublem3  16085  log2ublog2  16086  clwwlkn0  16649  clwwlk0on0  16672  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  konigsberg  16734  1kp2ke3k  16738  ex-fac  16742  depindlem1  16747  012of  17023  isomninnlem  17079  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102