ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0nn0 Unicode version

Theorem 0nn0 8370
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0  |-  0  e.  NN0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2082 . 2  |-  0  =  0
2 elnn0 8357 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 131 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 688 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 7 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 662    = wceq 1285    e. wcel 1434   0cc0 7043   NNcn 8106   NN0cn0 8355
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-1cn 7131  ax-icn 7133  ax-addcl 7134  ax-mulcl 7136  ax-i2m1 7143
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-n0 8356
This theorem is referenced by:  0xnn0  8424  elnn0z  8445  nn0ind-raph  8545  10nn0  8575  declei  8593  numlti  8594  nummul1c  8606  decaddc2  8613  decrmanc  8614  decrmac  8615  decaddm10  8616  decaddi  8617  decaddci  8618  decaddci2  8619  decmul1  8621  decmulnc  8624  6p5e11  8630  7p4e11  8633  8p3e11  8638  9p2e11  8644  10p10e20  8652  fz01or  9204  0elfz  9209  4fvwrd4  9227  fvinim0ffz  9327  exple1  9629  sq10  9737  bc0k  9780  bcn1  9782  bccl  9791  sizeeq0  9818  nn0o  10451  ndvdssub  10474  gcdval  10495  gcdcl  10502  dfgcd3  10543  nn0seqcvgd  10567  ialgcvg  10574  eucialg  10585  lcmcl  10598  pw2dvdslemn  10687  1kp2ke3k  10713  ex-fac  10716
  Copyright terms: Public domain W3C validator