Theorem 1nn0 9151

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 8889	. 2 |- 1 e. NN
2	1	nnnn0i 9143	1 |- 1 e. NN0

Syntax hints:   e. wcel 2141   1c1 7775   NN0cn0 9135

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-int 3832  df-inn 8879  df-n0 9136

This theorem is referenced by:  peano2nn0  9175  deccl  9357  10nn0  9360  numsucc  9382  numadd  9389  numaddc  9390  11multnc  9410  6p5lem  9412  6p6e12  9416  7p5e12  9419  8p4e12  9424  9p2e11  9429  9p3e12  9430  10p10e20  9437  4t4e16  9441  5t2e10  9442  5t4e20  9444  6t3e18  9447  6t4e24  9448  7t3e21  9452  7t4e28  9453  8t3e24  9458  9t3e27  9465  9t9e81  9471  nn01to3  9576  fz0to3un2pr  10079  elfzom1elp1fzo  10158  fzo0sn0fzo1  10177  1tonninf  10396  expn1ap0  10486  nn0expcl  10490  sqval  10534  sq10  10646  nn0opthlem1d  10654  fac2  10665  bccl  10701  hashsng  10733  1elfz0hash  10741  bcxmas  11452  arisum  11461  geoisum1  11482  geoisum1c  11483  cvgratnnlemsumlt  11491  mertenslem2  11499  fprodnn0cl  11575  ege2le3  11634  ef4p  11657  efgt1p2  11658  efgt1p  11659  sin01gt0  11724  dvds1  11813  3dvds2dec  11825  isprm5  12096  pcelnn  12274  pockthg  12309  ennnfonelemhom  12370  dsndx  12576  dsid  12577  dsslid  12578  dveflem  13481  1kp2ke3k  13759  ex-exp  13762  ex-fac  13763  012of  14028  isomninnlem  14062  trilpolemisumle  14070  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084