Theorem 0nn0 9129

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 2165	. 2 |- 0 = 0
2		elnn0 9116	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 132	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 726	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 698   = wceq 1343   e. wcel 2136   0cc0 7753   NNcn 8857   NN0cn0 9114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1cn 7846  ax-icn 7848  ax-addcl 7849  ax-mulcl 7851  ax-i2m1 7858

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-n0 9115

This theorem is referenced by:  0xnn0  9183  elnn0z  9204  nn0ind-raph  9308  10nn0  9339  declei  9357  numlti  9358  nummul1c  9370  decaddc2  9377  decrmanc  9378  decrmac  9379  decaddm10  9380  decaddi  9381  decaddci  9382  decaddci2  9383  decmul1  9385  decmulnc  9388  6p5e11  9394  7p4e11  9397  8p3e11  9402  9p2e11  9408  10p10e20  9416  fz01or  10046  0elfz  10053  4fvwrd4  10075  fvinim0ffz  10176  0tonninf  10374  exple1  10511  sq10  10625  bc0k  10669  bcn1  10671  bccl  10680  fihasheq0  10707  fsumnn0cl  11344  binom  11425  bcxmas  11430  isumnn0nn  11434  geoserap  11448  ef0lem  11601  ege2le3  11612  ef4p  11635  efgt1p2  11636  efgt1p  11637  nn0o  11844  ndvdssub  11867  gcdval  11892  gcdcl  11899  dfgcd3  11943  nn0seqcvgd  11973  algcvg  11980  eucalg  11991  lcmcl  12004  pw2dvdslemn  12097  pclem0  12218  pcpre1  12224  pcfac  12280  ennnfonelemj0  12334  ennnfonelem0  12338  ennnfonelem1  12340  dveflem  13327  pilem3  13344  1kp2ke3k  13605  ex-fac  13609  012of  13875  isomninnlem  13909  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931