Theorem 0nn0 9255

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 2193	. 2 |- 0 = 0
2		elnn0 9242	. . . 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 737	. 2 |- ( 0 = 0 -> 0 e. NN0 )
5	1, 4	ax-mp 5	1 |- 0 e. NN0

Syntax hints:   \/ wo 709   = wceq 1364   e. wcel 2164   0cc0 7872   NNcn 8982   NN0cn0 9240

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-n0 9241

This theorem is referenced by:  0xnn0  9309  elnn0z  9330  nn0ind-raph  9434  10nn0  9465  declei  9483  numlti  9484  nummul1c  9496  decaddc2  9503  decrmanc  9504  decrmac  9505  decaddm10  9506  decaddi  9507  decaddci  9508  decaddci2  9509  decmul1  9511  decmulnc  9514  6p5e11  9520  7p4e11  9523  8p3e11  9528  9p2e11  9534  10p10e20  9542  fz01or  10177  0elfz  10184  4fvwrd4  10206  fvinim0ffz  10308  0tonninf  10511  exple1  10666  sq10  10783  bc0k  10827  bcn1  10829  bccl  10838  fihasheq0  10864  iswrdiz  10921  iswrddm0  10938  fsumnn0cl  11546  binom  11627  bcxmas  11632  isumnn0nn  11636  geoserap  11650  ef0lem  11803  ege2le3  11814  ef4p  11837  efgt1p2  11838  efgt1p  11839  nn0o  12048  ndvdssub  12071  gcdval  12096  gcdcl  12103  dfgcd3  12147  nn0seqcvgd  12179  algcvg  12186  eucalg  12197  lcmcl  12210  pw2dvdslemn  12303  pclem0  12424  pcpre1  12430  pcfac  12488  ennnfonelemj0  12558  ennnfonelem0  12562  ennnfonelem1  12564  slotsdifdsndx  12838  slotsdifunifndx  12845  nn0subm  14071  znf1o  14139  fczpsrbag  14157  dveflem  14872  plyconst  14891  pilem3  14918  1kp2ke3k  15216  ex-fac  15220  012of  15486  isomninnlem  15520  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542