Theorem 1nn0 9192

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 8930	. 2 |- 1 e. NN
2	1	nnnn0i 9184	1 |- 1 e. NN0

Syntax hints:   e. wcel 2148   1c1 7812   NN0cn0 9176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7905

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-int 3846  df-inn 8920  df-n0 9177

This theorem is referenced by:  peano2nn0  9216  deccl  9398  10nn0  9401  numsucc  9423  numadd  9430  numaddc  9431  11multnc  9451  6p5lem  9453  6p6e12  9457  7p5e12  9460  8p4e12  9465  9p2e11  9470  9p3e12  9471  10p10e20  9478  4t4e16  9482  5t2e10  9483  5t4e20  9485  6t3e18  9488  6t4e24  9489  7t3e21  9493  7t4e28  9494  8t3e24  9499  9t3e27  9506  9t9e81  9512  nn01to3  9617  fz0to3un2pr  10123  elfzom1elp1fzo  10202  fzo0sn0fzo1  10221  1tonninf  10440  expn1ap0  10530  nn0expcl  10534  sqval  10578  sq10  10692  nn0opthlem1d  10700  fac2  10711  bccl  10747  hashsng  10778  1elfz0hash  10786  bcxmas  11497  arisum  11506  geoisum1  11527  geoisum1c  11528  cvgratnnlemsumlt  11536  mertenslem2  11544  fprodnn0cl  11620  ege2le3  11679  ef4p  11702  efgt1p2  11703  efgt1p  11704  sin01gt0  11769  dvds1  11859  3dvds2dec  11871  isprm5  12142  pcelnn  12320  pockthg  12355  ennnfonelemhom  12416  dsndx  12666  dsid  12667  dsslid  12668  dsndxnn  12669  basendxltdsndx  12670  slotsdifdsndx  12676  unifndx  12677  unifid  12678  unifndxnn  12679  basendxltunifndx  12680  slotsdifunifndx  12683  homid  12684  homslid  12685  ccoid  12686  ccoslid  12687  cnfldstr  13460  dveflem  14190  1kp2ke3k  14479  ex-exp  14482  ex-fac  14483  012of  14748  isomninnlem  14781  trilpolemisumle  14789  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803