Theorem 1nn0 9259

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 8995	. 2 |- 1 e. NN
2	1	nnnn0i 9251	1 |- 1 e. NN0

Syntax hints:   e. wcel 2164   1c1 7875   NN0cn0 9243

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7968

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-int 3872  df-inn 8985  df-n0 9244

This theorem is referenced by:  peano2nn0  9283  deccl  9465  10nn0  9468  numsucc  9490  numadd  9497  numaddc  9498  11multnc  9518  6p5lem  9520  6p6e12  9524  7p5e12  9527  8p4e12  9532  9p2e11  9537  9p3e12  9538  10p10e20  9545  4t4e16  9549  5t2e10  9550  5t4e20  9552  6t3e18  9555  6t4e24  9556  7t3e21  9560  7t4e28  9561  8t3e24  9566  9t3e27  9573  9t9e81  9579  nn01to3  9685  fz0to3un2pr  10192  elfzom1elp1fzo  10272  fzo0sn0fzo1  10291  fldiv4lem1div2  10379  1tonninf  10515  expn1ap0  10623  nn0expcl  10627  sqval  10671  sq10  10786  nn0opthlem1d  10794  fac2  10805  bccl  10841  hashsng  10872  1elfz0hash  10880  snopiswrd  10927  wrdred1hash  10960  bcxmas  11635  arisum  11644  geoisum1  11665  geoisum1c  11666  cvgratnnlemsumlt  11674  mertenslem2  11682  fprodnn0cl  11758  ege2le3  11817  ef4p  11840  efgt1p2  11841  efgt1p  11842  sin01gt0  11908  dvds1  11998  3dvds2dec  12010  isprm5  12283  pcelnn  12462  pockthg  12498  ennnfonelemhom  12575  dsndx  12831  dsid  12832  dsslid  12833  dsndxnn  12834  basendxltdsndx  12835  slotsdifdsndx  12841  unifndx  12842  unifid  12843  unifndxnn  12844  basendxltunifndx  12845  slotsdifunifndx  12848  homid  12849  homslid  12850  ccoid  12851  ccoslid  12852  cnfldstr  14057  dveflem  14905  plyid  14925  2lgslem3a  15250  2lgslem3c  15252  1kp2ke3k  15286  ex-exp  15289  ex-fac  15290  012of  15556  isomninnlem  15590  trilpolemisumle  15598  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612