Theorem 0nn0 9589

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 2238	. 2 |- 0 = 0
2		elnn0 9576	. . . 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 748	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

This proof depends on syntax axioms:   \/ wo 720   = wceq 1402   e. wcel 2209   0cc0 8185   NNcn 9313   NN0cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-n0 9575

This theorem is used by:  0xnn0  9645  elnn0z  9666  fcdmnn0fsuppfi  9743  nn0ind-raph  9773  10nn0  9808  declei  9827  numlti  9828  nummul1c  9840  decaddc2  9847  decrmanc  9848  decrmac  9849  decaddm10  9850  decaddi  9851  decaddci  9852  decaddci2  9853  decmul1  9855  decmulnc  9858  6p5e11  9864  7p4e11  9867  8p3e11  9872  9p2e11  9878  10p10e20  9886  fz01or  10534  0elfz  10541  4fvwrd4  10563  fvinim0ffz  10676  0tonninf  10897  exple1  11052  sq10  11171  bc0k  11215  bcn1  11217  bccl  11226  fihasheq0  11253  hashfibc  11304  iswrdiz  11332  iswrddm0  11349  s1leng  11413  s1fv  11415  eqs1  11417  s111  11420  ccat2s1fstg  11437  pfx00g  11468  s2fv0g  11580  s3fv0g  11584  fsumnn0cl  12194  binom  12275  bcxmas  12280  isumnn0nn  12284  geoserap  12298  ef0lem  12451  ege2le3  12462  ef4p  12485  efgt1p2  12486  efgt1p  12487  nn0o  12698  ndvdssub  12721  5ndvds3  12725  bits0  12739  0bits  12750  gcdval  12760  gcdcl  12767  dfgcd3  12811  nn0seqcvgd  12843  algcvg  12850  eucalg  12861  lcmcl  12874  pwbdvdslemn  12968  pclem0  13093  pcpre1  13099  pcfac  13157  dec5dvds2  13220  2exp11  13244  2exp16  13245  10nprm  13256  11prm  13257  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  ennnfonelemj0  13349  ennnfonelem0  13353  ennnfonelem1  13355  plendxnocndx  13626  slotsdifdsndx  13637  slotsdifunifndx  13644  imasvalstrd  13677  gsum0cmn  14243  cnfldstr  15003  nn0subm  15028  znf1o  15094  snifpsrbagfi  15168  fczpsrbag  15169  psrbagmaxlem1  15178  psr1clfi  15207  psrlidmfi  15208  mvrclfi  15226  dveflem  15969  plyconst  15988  plycolemc  16001  pilem3  16027  log2ublem3  16240  log2ublog2  16241  ppiublem2  16309  chtublem  16312  bclbnd  16324  bposlem8  16335  clwwlkn0  16871  clwwlk0on0  16894  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  konigsberg  16956  1kp2ke3k  16960  ex-fac  16964  depindlem1  16969  012of  17245  isomninnlem  17302  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326