Theorem 1nn0 8371

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	|- 1 e. NN0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 8117	. 2 |- 1 e. NN
2	1	nnnn0i 8363	1 |- 1 e. NN0

Syntax hints:   e. wcel 1434   1c1 7044   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-1re 7132

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-ral 2354  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-int 3645  df-inn 8107  df-n0 8356

This theorem is referenced by:  peano2nn0  8395  deccl  8572  10nn0  8575  numsucc  8597  numadd  8604  numaddc  8605  11multnc  8625  6p5lem  8627  6p6e12  8631  7p5e12  8634  8p4e12  8639  9p2e11  8644  9p3e12  8645  10p10e20  8652  4t4e16  8656  5t2e10  8657  5t4e20  8659  6t3e18  8662  6t4e24  8663  7t3e21  8667  7t4e28  8668  8t3e24  8673  9t3e27  8680  9t9e81  8686  nn01to3  8783  elfzom1elp1fzo  9288  fzo0sn0fzo1  9307  expn1ap0  9583  nn0expcl  9587  sqval  9631  sq10  9737  nn0opthlem1d  9744  fac2  9755  bccl  9791  sizesng  9822  1elfz0size  9830  dvds1  10398  3dvds2dec  10410  1kp2ke3k  10713  ex-fac  10716