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

Theorem 1nn0 8255
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 8001 . 2 1 ∈ ℕ
21nnnn0i 8247 1 1 ∈ ℕ0
Colors of variables: wff set class
Syntax hints:  wcel 1409  1c1 6948  0cn0 8239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-1re 7036
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-int 3644  df-inn 7991  df-n0 8240
This theorem is referenced by:  peano2nn0  8279  deccl  8441  10nn0  8444  numsucc  8466  numadd  8473  numaddc  8474  11multnc  8494  6p5lem  8496  6p6e12  8500  7p5e12  8503  8p4e12  8508  9p2e11  8513  9p3e12  8514  10p10e20  8521  4t4e16  8525  5t2e10  8526  5t4e20  8528  6t3e18  8531  6t4e24  8532  7t3e21  8536  7t4e28  8537  8t3e24  8542  9t3e27  8549  9t9e81  8555  nn01to3  8649  elfzom1elp1fzo  9160  fzo0sn0fzo1  9179  expn1ap0  9430  nn0expcl  9434  sqval  9478  sq10  9584  nn0opthlem1d  9588  fac2  9599  bccl  9635  dvds1  10165  3dvds2dec  10177  1kp2ke3k  10278  ex-fac  10281
  Copyright terms: Public domain W3C validator