Theorem 0nn0 8890

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 2113	. 2 |- 0 = 0
2		elnn0 8877	. . . 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 708	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 7	1 |- 0 e. NN0

Syntax hints:   \/ wo 680   = wceq 1312   e. wcel 1461   0cc0 7541   NNcn 8624   NN0cn0 8875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-1cn 7632  ax-icn 7634  ax-addcl 7635  ax-mulcl 7637  ax-i2m1 7644

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-sn 3497  df-n0 8876

This theorem is referenced by:  0xnn0  8944  elnn0z  8965  nn0ind-raph  9066  10nn0  9097  declei  9115  numlti  9116  nummul1c  9128  decaddc2  9135  decrmanc  9136  decrmac  9137  decaddm10  9138  decaddi  9139  decaddci  9140  decaddci2  9141  decmul1  9143  decmulnc  9146  6p5e11  9152  7p4e11  9155  8p3e11  9160  9p2e11  9166  10p10e20  9174  fz01or  9778  0elfz  9785  4fvwrd4  9804  fvinim0ffz  9905  0tonninf  10099  exple1  10236  sq10  10346  bc0k  10389  bcn1  10391  bccl  10400  fihasheq0  10427  fsumnn0cl  11058  binom  11139  bcxmas  11144  isumnn0nn  11148  geoserap  11162  ef0lem  11211  ege2le3  11222  ef4p  11245  efgt1p2  11246  efgt1p  11247  nn0o  11446  ndvdssub  11469  gcdval  11490  gcdcl  11497  dfgcd3  11538  nn0seqcvgd  11562  algcvg  11569  eucalg  11580  lcmcl  11593  pw2dvdslemn  11682  ennnfonelemj0  11753  ennnfonelem0  11757  ennnfonelem1  11759  1kp2ke3k  12620  ex-fac  12624  isomninnlem  12906