Theorem 1nn0 9529

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 9265	. 2 |- 1 e. NN
2	1	nnnn0i 9521	1 |- 1 e. NN0

Syntax hints:   e. wcel 2205   1c1 8144   NN0cn0 9513

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-int 3955  df-inn 9255  df-n0 9514

This theorem is referenced by:  peano2nn0  9553  deccl  9741  10nn0  9744  numsucc  9766  numadd  9773  numaddc  9774  11multnc  9794  6p5lem  9796  6p6e12  9800  7p5e12  9803  8p4e12  9808  9p2e11  9813  9p3e12  9814  10p10e20  9821  4t4e16  9825  5t2e10  9826  5t4e20  9828  6t3e18  9831  6t4e24  9832  7t3e21  9836  7t4e28  9837  8t3e24  9842  9t3e27  9849  9t9e81  9855  nn01to3  9967  fz0to3un2pr  10479  elfzom1elp1fzo  10569  fzo0sn0fzo1  10588  fldiv4lem1div2  10691  1tonninf  10827  expn1ap0  10935  nn0expcl  10939  sqval  10983  sq10  11099  nn0opthlem1d  11107  fac2  11118  bccl  11154  hashsng  11186  1elfz0hash  11196  snopiswrd  11259  wrdred1hash  11293  pfx1  11420  s3fv1g  11509  bcxmas  12200  arisum  12209  geoisum1  12230  geoisum1c  12231  cvgratnnlemsumlt  12239  mertenslem2  12247  fprodnn0cl  12323  ege2le3  12382  ef4p  12405  efgt1p2  12406  efgt1p  12407  sin01gt0  12473  dvds1  12564  3dvds2dec  12577  5ndvds6  12646  bitsmod  12667  bitsinv1lem  12672  isprm5  12864  pcelnn  13044  pockthg  13080  dec5nprm  13137  dec2nprm  13138  modxp1i  13141  2exp8  13158  2exp11  13159  2exp16  13160  2expltfac  13162  ennnfonelemhom  13250  ocndx  13508  ocid  13509  basendxnocndx  13510  plendxnocndx  13511  dsndx  13512  dsid  13513  dsslid  13514  dsndxnn  13515  basendxltdsndx  13516  slotsdifdsndx  13522  unifndx  13523  unifid  13524  unifndxnn  13525  basendxltunifndx  13526  slotsdifunifndx  13529  homndx  13530  homid  13531  homslid  13532  ccondx  13533  ccoid  13534  ccoslid  13535  imasvalstrd  13562  prdsvalstrd  13563  cnfldstr  14832  dveflem  15717  plyid  15737  1sgmprm  15988  perfectlem1  15993  perfectlem2  15994  2lgslem3a  16092  2lgslem3c  16094  edgfid  16127  edgfndx  16128  edgfndxnn  16129  basendxltedgfndx  16131  clwwlkccatlem  16521  umgr2cwwkdifex  16546  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem4  16612  konigsberglem5  16613  konigsberg  16614  1kp2ke3k  16618  ex-exp  16621  ex-fac  16622  012of  16893  isomninnlem  16940  trilpolemisumle  16948  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963