Theorem 0nn0 8621

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 2085	. 2 |- 0 = 0
2		elnn0 8608	. . . 4 |- ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3	2	biimpri 131	. . 3 |- ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4	3	olcs 688	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 7	1 |- 0 e. NN0

Syntax hints:   \/ wo 662   = wceq 1287   e. wcel 1436   0cc0 7294   NNcn 8357   NN0cn0 8606

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1cn 7382  ax-icn 7384  ax-addcl 7385  ax-mulcl 7387  ax-i2m1 7394

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-n0 8607

This theorem is referenced by:  0xnn0  8675  elnn0z  8696  nn0ind-raph  8796  10nn0  8826  declei  8844  numlti  8845  nummul1c  8857  decaddc2  8864  decrmanc  8865  decrmac  8866  decaddm10  8867  decaddi  8868  decaddci  8869  decaddci2  8870  decmul1  8872  decmulnc  8875  6p5e11  8881  7p4e11  8884  8p3e11  8889  9p2e11  8895  10p10e20  8903  fz01or  9455  0elfz  9460  4fvwrd4  9479  fvinim0ffz  9580  0tonninf  9773  exple1  9909  sq10  10017  bc0k  10060  bcn1  10062  bccl  10071  fihasheq0  10098  nn0o  10782  ndvdssub  10805  gcdval  10826  gcdcl  10833  dfgcd3  10874  nn0seqcvgd  10898  ialgcvg  10905  eucialg  10916  lcmcl  10929  pw2dvdslemn  11018  1kp2ke3k  11090  ex-fac  11093