Theorem 0nn0 9557

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 9544	. . . 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

Syntax hints:   \/ wo 720   = wceq 1402   e. wcel 2209   0cc0 8169   NNcn 9283   NN0cn0 9542

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 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 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274

This theorem 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 3711  df-n0 9543

This theorem is referenced by:  0xnn0  9615  elnn0z  9636  nn0ind-raph  9742  10nn0  9773  declei  9791  numlti  9792  nummul1c  9804  decaddc2  9811  decrmanc  9812  decrmac  9813  decaddm10  9814  decaddi  9815  decaddci  9816  decaddci2  9817  decmul1  9819  decmulnc  9822  6p5e11  9828  7p4e11  9831  8p3e11  9836  9p2e11  9842  10p10e20  9850  fz01or  10496  0elfz  10503  4fvwrd4  10525  fvinim0ffz  10638  0tonninf  10855  exple1  11010  sq10  11128  bc0k  11172  bcn1  11174  bccl  11183  fihasheq0  11210  hashfibc  11261  iswrdiz  11289  iswrddm0  11306  s1leng  11370  s1fv  11372  eqs1  11374  s111  11377  ccat2s1fstg  11394  pfx00g  11425  s2fv0g  11537  s3fv0g  11541  fsumnn0cl  12148  binom  12229  bcxmas  12234  isumnn0nn  12238  geoserap  12252  ef0lem  12405  ege2le3  12416  ef4p  12439  efgt1p2  12440  efgt1p  12441  nn0o  12652  ndvdssub  12675  5ndvds3  12679  bits0  12693  0bits  12704  gcdval  12714  gcdcl  12721  dfgcd3  12765  nn0seqcvgd  12797  algcvg  12804  eucalg  12815  lcmcl  12828  pw2dvdslemn  12921  pclem0  13043  pcpre1  13049  pcfac  13107  dec5dvds2  13170  2exp11  13193  2exp16  13194  ennnfonelemj0  13270  ennnfonelem0  13274  ennnfonelem1  13276  plendxnocndx  13545  slotsdifdsndx  13556  slotsdifunifndx  13563  imasvalstrd  13596  gsum0cmn  14131  cnfldstr  14867  nn0subm  14892  znf1o  14958  fczpsrbag  14979  psr1clfi  15002  mplsubgfilemm  15012  dveflem  15750  plyconst  15769  plycolemc  15782  pilem3  15807  clwwlkn0  16563  clwwlk0on0  16586  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  konigsberg  16648  1kp2ke3k  16652  ex-fac  16656  depindlem1  16661  012of  16937  isomninnlem  16984  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007