Theorem 0nn0 9164

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 2175	. 2 |- 0 = 0
2		elnn0 9151	. . . 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 736	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 708   = wceq 1353   e. wcel 2146   0cc0 7786   NNcn 8892   NN0cn0 9149

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-1cn 7879  ax-icn 7881  ax-addcl 7882  ax-mulcl 7884  ax-i2m1 7891

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-n0 9150

This theorem is referenced by:  0xnn0  9218  elnn0z  9239  nn0ind-raph  9343  10nn0  9374  declei  9392  numlti  9393  nummul1c  9405  decaddc2  9412  decrmanc  9413  decrmac  9414  decaddm10  9415  decaddi  9416  decaddci  9417  decaddci2  9418  decmul1  9420  decmulnc  9423  6p5e11  9429  7p4e11  9432  8p3e11  9437  9p2e11  9443  10p10e20  9451  fz01or  10081  0elfz  10088  4fvwrd4  10110  fvinim0ffz  10211  0tonninf  10409  exple1  10546  sq10  10660  bc0k  10704  bcn1  10706  bccl  10715  fihasheq0  10741  fsumnn0cl  11379  binom  11460  bcxmas  11465  isumnn0nn  11469  geoserap  11483  ef0lem  11636  ege2le3  11647  ef4p  11670  efgt1p2  11671  efgt1p  11672  nn0o  11879  ndvdssub  11902  gcdval  11927  gcdcl  11934  dfgcd3  11978  nn0seqcvgd  12008  algcvg  12015  eucalg  12026  lcmcl  12039  pw2dvdslemn  12132  pclem0  12253  pcpre1  12259  pcfac  12315  ennnfonelemj0  12369  ennnfonelem0  12373  ennnfonelem1  12375  slotsdifdsndx  12609  dveflem  13758  pilem3  13775  1kp2ke3k  14036  ex-fac  14040  012of  14305  isomninnlem  14339  iswomninnlem  14358  iswomni0  14360  ismkvnnlem  14361