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

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

Proof of Theorem 1nn0
StepHypRef Expression
1 1nn 7798 . 2 1
21nnnn0i 8057 1 1 0
Colors of variables: wff set class
Syntax hints:   wcel 1393  1c1 6780  0cn0 8049
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-1re 6868
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-ral 2308  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-int 3610  df-inn 7788  df-n0 8050
This theorem is referenced by:  peano2nn0  8090  numsucc  8261  numadd  8269  numaddc  8270  6p5lem  8284  6p6e12  8286  7p5e12  8288  8p4e12  8292  9p2e11  8297  9p3e12  8298  10p10e20  8305  4t4e16  8308  5t4e20  8310  6t3e18  8313  6t4e24  8314  7t3e21  8318  7t4e28  8319  8t3e24  8324  9t3e27  8331  9t9e81  8337  nn01to3  8420  elfzom1elp1fzo  8920  fzo0sn0fzo1  8939  expn1ap0  9012  nn0expcl  9016  sqval  9059
  Copyright terms: Public domain W3C validator