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

Theorem 0nn0 8196
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 2040 . 2  |-  0  =  0
2 elnn0 8183 . . . 4  |-  ( 0  e.  NN0  <->  ( 0  e.  NN  \/  0  =  0 ) )
32biimpri 124 . . 3  |-  ( ( 0  e.  NN  \/  0  =  0 )  ->  0  e.  NN0 )
43olcs 655 . 2  |-  ( 0  =  0  ->  0  e.  NN0 )
51, 4ax-mp 7 1  |-  0  e.  NN0
Colors of variables: wff set class
Syntax hints:    \/ wo 629    = wceq 1243    e. wcel 1393   0cc0 6889   NNcn 7914   NN0cn0 8181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-1cn 6977  ax-icn 6979  ax-addcl 6980  ax-mulcl 6982  ax-i2m1 6989
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-sn 3381  df-n0 8182
This theorem is referenced by:  elnn0z  8258  nn0ind-raph  8355  numlti  8391  nummul1c  8403  decaddc2  8410  decaddi  8411  decaddci  8412  decaddci2  8413  6p5e11  8417  7p4e11  8419  8p3e11  8423  9p2e11  8429  10p10e20  8437  0elfz  8977  4fvwrd4  8997  fvinim0ffz  9096  exple1  9310  nn0seqcvgd  9880  ialgcvg  9887
  Copyright terms: Public domain W3C validator