Theorem 1nn0 9085

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 8823	. 2 |- 1 e. NN
2	1	nnnn0i 9077	1 |- 1 e. NN0

Syntax hints:   e. wcel 2125   1c1 7712   NN0cn0 9069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136  ax-1re 7805

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-v 2711  df-un 3102  df-in 3104  df-ss 3111  df-int 3804  df-inn 8813  df-n0 9070

This theorem is referenced by:  peano2nn0  9109  deccl  9288  10nn0  9291  numsucc  9313  numadd  9320  numaddc  9321  11multnc  9341  6p5lem  9343  6p6e12  9347  7p5e12  9350  8p4e12  9355  9p2e11  9360  9p3e12  9361  10p10e20  9368  4t4e16  9372  5t2e10  9373  5t4e20  9375  6t3e18  9378  6t4e24  9379  7t3e21  9383  7t4e28  9384  8t3e24  9389  9t3e27  9396  9t9e81  9402  nn01to3  9504  elfzom1elp1fzo  10079  fzo0sn0fzo1  10098  1tonninf  10317  expn1ap0  10407  nn0expcl  10411  sqval  10455  sq10  10563  nn0opthlem1d  10571  fac2  10582  bccl  10618  hashsng  10649  1elfz0hash  10657  bcxmas  11363  arisum  11372  geoisum1  11393  geoisum1c  11394  cvgratnnlemsumlt  11402  mertenslem2  11410  fprodnn0cl  11486  ege2le3  11545  ef4p  11568  efgt1p2  11569  efgt1p  11570  sin01gt0  11635  dvds1  11718  3dvds2dec  11730  ennnfonelemhom  12103  dsndx  12295  dsid  12296  dsslid  12297  dveflem  13034  1kp2ke3k  13246  ex-exp  13249  ex-fac  13250  012of  13514  isomninnlem  13550  trilpolemisumle  13558  iswomninnlem  13569  iswomni0  13571  ismkvnnlem  13572