Theorem 0nn0 9476

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 2231	. 2 |- 0 = 0
2		elnn0 9463	. . . 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 744	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 716   = wceq 1398   e. wcel 2202   0cc0 8092   NNcn 9202   NN0cn0 9461

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1cn 8185  ax-icn 8187  ax-addcl 8188  ax-mulcl 8190  ax-i2m1 8197

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-n0 9462

This theorem is referenced by:  0xnn0  9532  elnn0z  9553  nn0ind-raph  9658  10nn0  9689  declei  9707  numlti  9708  nummul1c  9720  decaddc2  9727  decrmanc  9728  decrmac  9729  decaddm10  9730  decaddi  9731  decaddci  9732  decaddci2  9733  decmul1  9735  decmulnc  9738  6p5e11  9744  7p4e11  9747  8p3e11  9752  9p2e11  9758  10p10e20  9766  fz01or  10408  0elfz  10415  4fvwrd4  10437  fvinim0ffz  10550  0tonninf  10765  exple1  10920  sq10  11037  bc0k  11081  bcn1  11083  bccl  11092  fihasheq0  11118  iswrdiz  11186  iswrddm0  11203  s1leng  11267  s1fv  11269  eqs1  11271  s111  11274  ccat2s1fstg  11291  pfx00g  11322  s2fv0g  11434  s3fv0g  11438  fsumnn0cl  12044  binom  12125  bcxmas  12130  isumnn0nn  12134  geoserap  12148  ef0lem  12301  ege2le3  12312  ef4p  12335  efgt1p2  12336  efgt1p  12337  nn0o  12548  ndvdssub  12571  5ndvds3  12575  bits0  12589  0bits  12600  gcdval  12610  gcdcl  12617  dfgcd3  12661  nn0seqcvgd  12693  algcvg  12700  eucalg  12711  lcmcl  12724  pw2dvdslemn  12817  pclem0  12939  pcpre1  12945  pcfac  13003  dec5dvds2  13066  2exp11  13089  2exp16  13090  ennnfonelemj0  13102  ennnfonelem0  13106  ennnfonelem1  13108  plendxnocndx  13377  slotsdifdsndx  13388  slotsdifunifndx  13395  imasvalstrd  13433  cnfldstr  14654  nn0subm  14679  znf1o  14747  fczpsrbag  14767  psr1clfi  14789  mplsubgfilemm  14799  dveflem  15537  plyconst  15556  plycolemc  15569  pilem3  15594  clwwlkn0  16349  clwwlk0on0  16372  konigsberglem2  16430  konigsberglem3  16431  konigsberglem5  16433  konigsberg  16434  1kp2ke3k  16438  ex-fac  16442  depindlem1  16447  012of  16713  isomninnlem  16762  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785  gfsum0  16811