Theorem 1nn0 9194

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 8932	. 2 |- 1 e. NN
2	1	nnnn0i 9186	1 |- 1 e. NN0

Syntax hints:   e. wcel 2148   1c1 7814   NN0cn0 9178

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 7907

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 2741  df-un 3135  df-in 3137  df-ss 3144  df-int 3847  df-inn 8922  df-n0 9179

This theorem is referenced by:  peano2nn0  9218  deccl  9400  10nn0  9403  numsucc  9425  numadd  9432  numaddc  9433  11multnc  9453  6p5lem  9455  6p6e12  9459  7p5e12  9462  8p4e12  9467  9p2e11  9472  9p3e12  9473  10p10e20  9480  4t4e16  9484  5t2e10  9485  5t4e20  9487  6t3e18  9490  6t4e24  9491  7t3e21  9495  7t4e28  9496  8t3e24  9501  9t3e27  9508  9t9e81  9514  nn01to3  9619  fz0to3un2pr  10125  elfzom1elp1fzo  10204  fzo0sn0fzo1  10223  1tonninf  10442  expn1ap0  10532  nn0expcl  10536  sqval  10580  sq10  10694  nn0opthlem1d  10702  fac2  10713  bccl  10749  hashsng  10780  1elfz0hash  10788  bcxmas  11499  arisum  11508  geoisum1  11529  geoisum1c  11530  cvgratnnlemsumlt  11538  mertenslem2  11546  fprodnn0cl  11622  ege2le3  11681  ef4p  11704  efgt1p2  11705  efgt1p  11706  sin01gt0  11771  dvds1  11861  3dvds2dec  11873  isprm5  12144  pcelnn  12322  pockthg  12357  ennnfonelemhom  12418  dsndx  12671  dsid  12672  dsslid  12673  dsndxnn  12674  basendxltdsndx  12675  slotsdifdsndx  12681  unifndx  12682  unifid  12683  unifndxnn  12684  basendxltunifndx  12685  slotsdifunifndx  12688  homid  12689  homslid  12690  ccoid  12691  ccoslid  12692  cnfldstr  13542  dveflem  14272  1kp2ke3k  14561  ex-exp  14564  ex-fac  14565  012of  14830  isomninnlem  14863  trilpolemisumle  14871  iswomninnlem  14882  iswomni0  14884  ismkvnnlem  14885