Theorem 0nn0 9384

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 2229	. 2 |- 0 = 0
2		elnn0 9371	. . . 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 741	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 713   = wceq 1395   e. wcel 2200   0cc0 7999   NNcn 9110   NN0cn0 9369

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8092  ax-icn 8094  ax-addcl 8095  ax-mulcl 8097  ax-i2m1 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9370

This theorem is referenced by:  0xnn0  9438  elnn0z  9459  nn0ind-raph  9564  10nn0  9595  declei  9613  numlti  9614  nummul1c  9626  decaddc2  9633  decrmanc  9634  decrmac  9635  decaddm10  9636  decaddi  9637  decaddci  9638  decaddci2  9639  decmul1  9641  decmulnc  9644  6p5e11  9650  7p4e11  9653  8p3e11  9658  9p2e11  9664  10p10e20  9672  fz01or  10307  0elfz  10314  4fvwrd4  10336  fvinim0ffz  10447  0tonninf  10662  exple1  10817  sq10  10934  bc0k  10978  bcn1  10980  bccl  10989  fihasheq0  11015  iswrdiz  11078  iswrddm0  11095  s1leng  11157  s1fv  11159  eqs1  11161  s111  11164  pfx00g  11207  s2fv0g  11319  s3fv0g  11323  fsumnn0cl  11914  binom  11995  bcxmas  12000  isumnn0nn  12004  geoserap  12018  ef0lem  12171  ege2le3  12182  ef4p  12205  efgt1p2  12206  efgt1p  12207  nn0o  12418  ndvdssub  12441  5ndvds3  12445  bits0  12459  0bits  12470  gcdval  12480  gcdcl  12487  dfgcd3  12531  nn0seqcvgd  12563  algcvg  12570  eucalg  12581  lcmcl  12594  pw2dvdslemn  12687  pclem0  12809  pcpre1  12815  pcfac  12873  dec5dvds2  12936  2exp11  12959  2exp16  12960  ennnfonelemj0  12972  ennnfonelem0  12976  ennnfonelem1  12978  plendxnocndx  13247  slotsdifdsndx  13258  slotsdifunifndx  13265  imasvalstrd  13303  cnfldstr  14522  nn0subm  14547  znf1o  14615  fczpsrbag  14635  psr1clfi  14652  mplsubgfilemm  14662  dveflem  15400  plyconst  15419  plycolemc  15432  pilem3  15457  1kp2ke3k  16088  ex-fac  16092  012of  16357  isomninnlem  16398  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420