Theorem 0nn0 9312

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 2205	. 2 |- 0 = 0
2		elnn0 9299	. . . 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 738	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 710   = wceq 1373   e. wcel 2176   0cc0 7927   NNcn 9038   NN0cn0 9297

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1cn 8020  ax-icn 8022  ax-addcl 8023  ax-mulcl 8025  ax-i2m1 8032

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-n0 9298

This theorem is referenced by:  0xnn0  9366  elnn0z  9387  nn0ind-raph  9492  10nn0  9523  declei  9541  numlti  9542  nummul1c  9554  decaddc2  9561  decrmanc  9562  decrmac  9563  decaddm10  9564  decaddi  9565  decaddci  9566  decaddci2  9567  decmul1  9569  decmulnc  9572  6p5e11  9578  7p4e11  9581  8p3e11  9586  9p2e11  9592  10p10e20  9600  fz01or  10235  0elfz  10242  4fvwrd4  10264  fvinim0ffz  10372  0tonninf  10587  exple1  10742  sq10  10859  bc0k  10903  bcn1  10905  bccl  10914  fihasheq0  10940  iswrdiz  11003  iswrddm0  11020  s1leng  11081  s1fv  11083  eqs1  11085  s111  11088  pfx00g  11131  fsumnn0cl  11747  binom  11828  bcxmas  11833  isumnn0nn  11837  geoserap  11851  ef0lem  12004  ege2le3  12015  ef4p  12038  efgt1p2  12039  efgt1p  12040  nn0o  12251  ndvdssub  12274  5ndvds3  12278  bits0  12292  0bits  12303  gcdval  12313  gcdcl  12320  dfgcd3  12364  nn0seqcvgd  12396  algcvg  12403  eucalg  12414  lcmcl  12427  pw2dvdslemn  12520  pclem0  12642  pcpre1  12648  pcfac  12706  dec5dvds2  12769  2exp11  12792  2exp16  12793  ennnfonelemj0  12805  ennnfonelem0  12809  ennnfonelem1  12811  plendxnocndx  13079  slotsdifdsndx  13090  slotsdifunifndx  13097  imasvalstrd  13135  cnfldstr  14353  nn0subm  14378  znf1o  14446  fczpsrbag  14466  psr1clfi  14483  mplsubgfilemm  14493  dveflem  15231  plyconst  15250  plycolemc  15263  pilem3  15288  1kp2ke3k  15697  ex-fac  15701  012of  15967  isomninnlem  16006  iswomninnlem  16025  iswomni0  16027  ismkvnnlem  16028