Theorem 1nn0 9265

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 9001	. 2 |- 1 e. NN
2	1	nnnn0i 9257	1 |- 1 e. NN0

Syntax hints:   e. wcel 2167   1c1 7880   NN0cn0 9249

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7973

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-int 3875  df-inn 8991  df-n0 9250

This theorem is referenced by:  peano2nn0  9289  deccl  9471  10nn0  9474  numsucc  9496  numadd  9503  numaddc  9504  11multnc  9524  6p5lem  9526  6p6e12  9530  7p5e12  9533  8p4e12  9538  9p2e11  9543  9p3e12  9544  10p10e20  9551  4t4e16  9555  5t2e10  9556  5t4e20  9558  6t3e18  9561  6t4e24  9562  7t3e21  9566  7t4e28  9567  8t3e24  9572  9t3e27  9579  9t9e81  9585  nn01to3  9691  fz0to3un2pr  10198  elfzom1elp1fzo  10278  fzo0sn0fzo1  10297  fldiv4lem1div2  10397  1tonninf  10533  expn1ap0  10641  nn0expcl  10645  sqval  10689  sq10  10804  nn0opthlem1d  10812  fac2  10823  bccl  10859  hashsng  10890  1elfz0hash  10898  snopiswrd  10945  wrdred1hash  10978  bcxmas  11654  arisum  11663  geoisum1  11684  geoisum1c  11685  cvgratnnlemsumlt  11693  mertenslem2  11701  fprodnn0cl  11777  ege2le3  11836  ef4p  11859  efgt1p2  11860  efgt1p  11861  sin01gt0  11927  dvds1  12018  3dvds2dec  12031  5ndvds6  12100  isprm5  12310  pcelnn  12490  pockthg  12526  dec5nprm  12583  dec2nprm  12584  modxp1i  12587  2exp8  12604  2exp11  12605  2exp16  12606  2expltfac  12608  ennnfonelemhom  12632  dsndx  12888  dsid  12889  dsslid  12890  dsndxnn  12891  basendxltdsndx  12892  slotsdifdsndx  12898  unifndx  12899  unifid  12900  unifndxnn  12901  basendxltunifndx  12902  slotsdifunifndx  12905  homid  12906  homslid  12907  ccoid  12908  ccoslid  12909  cnfldstr  14114  dveflem  14962  plyid  14982  1sgmprm  15230  perfectlem1  15235  perfectlem2  15236  2lgslem3a  15334  2lgslem3c  15336  1kp2ke3k  15370  ex-exp  15373  ex-fac  15374  012of  15640  isomninnlem  15674  trilpolemisumle  15682  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696