Theorem 1nn0 9512

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 9248	. 2 |- 1 e. NN
2	1	nnnn0i 9504	1 |- 1 e. NN0

Syntax hints:   e. wcel 2203   1c1 8128   NN0cn0 9496

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 2214  ax-1re 8221

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  peano2nn0  9536  deccl  9723  10nn0  9726  numsucc  9748  numadd  9755  numaddc  9756  11multnc  9776  6p5lem  9778  6p6e12  9782  7p5e12  9785  8p4e12  9790  9p2e11  9795  9p3e12  9796  10p10e20  9803  4t4e16  9807  5t2e10  9808  5t4e20  9810  6t3e18  9813  6t4e24  9814  7t3e21  9818  7t4e28  9819  8t3e24  9824  9t3e27  9831  9t9e81  9837  nn01to3  9949  fz0to3un2pr  10457  elfzom1elp1fzo  10547  fzo0sn0fzo1  10566  fldiv4lem1div2  10667  1tonninf  10803  expn1ap0  10911  nn0expcl  10915  sqval  10959  sq10  11074  nn0opthlem1d  11082  fac2  11093  bccl  11129  hashsng  11161  1elfz0hash  11171  snopiswrd  11234  wrdred1hash  11268  pfx1  11395  s3fv1g  11484  bcxmas  12175  arisum  12184  geoisum1  12205  geoisum1c  12206  cvgratnnlemsumlt  12214  mertenslem2  12222  fprodnn0cl  12298  ege2le3  12357  ef4p  12380  efgt1p2  12381  efgt1p  12382  sin01gt0  12448  dvds1  12539  3dvds2dec  12552  5ndvds6  12621  bitsmod  12642  bitsinv1lem  12647  isprm5  12839  pcelnn  13019  pockthg  13055  dec5nprm  13112  dec2nprm  13113  modxp1i  13116  2exp8  13133  2exp11  13134  2exp16  13135  2expltfac  13137  ennnfonelemhom  13166  ocndx  13424  ocid  13425  basendxnocndx  13426  plendxnocndx  13427  dsndx  13428  dsid  13429  dsslid  13430  dsndxnn  13431  basendxltdsndx  13432  slotsdifdsndx  13438  unifndx  13439  unifid  13440  unifndxnn  13441  basendxltunifndx  13442  slotsdifunifndx  13445  homndx  13446  homid  13447  homslid  13448  ccondx  13449  ccoid  13450  ccoslid  13451  imasvalstrd  13483  prdsvalstrd  13484  cnfldstr  14706  dveflem  15591  plyid  15611  1sgmprm  15862  perfectlem1  15867  perfectlem2  15868  2lgslem3a  15966  2lgslem3c  15968  edgfid  16001  edgfndx  16002  edgfndxnn  16003  basendxltedgfndx  16005  clwwlkccatlem  16395  umgr2cwwkdifex  16420  konigsbergiedgwen  16479  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem4  16486  konigsberglem5  16487  konigsberg  16488  1kp2ke3k  16492  ex-exp  16495  ex-fac  16496  012of  16767  isomninnlem  16814  trilpolemisumle  16822  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837