Theorem 1nn0 9418

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 9154	. 2 |- 1 e. NN
2	1	nnnn0i 9410	1 |- 1 e. NN0

Syntax hints:   e. wcel 2202   1c1 8033   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  peano2nn0  9442  deccl  9625  10nn0  9628  numsucc  9650  numadd  9657  numaddc  9658  11multnc  9678  6p5lem  9680  6p6e12  9684  7p5e12  9687  8p4e12  9692  9p2e11  9697  9p3e12  9698  10p10e20  9705  4t4e16  9709  5t2e10  9710  5t4e20  9712  6t3e18  9715  6t4e24  9716  7t3e21  9720  7t4e28  9721  8t3e24  9726  9t3e27  9733  9t9e81  9739  nn01to3  9851  fz0to3un2pr  10358  elfzom1elp1fzo  10447  fzo0sn0fzo1  10466  fldiv4lem1div2  10567  1tonninf  10703  expn1ap0  10811  nn0expcl  10815  sqval  10859  sq10  10974  nn0opthlem1d  10982  fac2  10993  bccl  11029  hashsng  11060  1elfz0hash  11070  snopiswrd  11123  wrdred1hash  11157  pfx1  11284  s3fv1g  11373  bcxmas  12051  arisum  12060  geoisum1  12081  geoisum1c  12082  cvgratnnlemsumlt  12090  mertenslem2  12098  fprodnn0cl  12174  ege2le3  12233  ef4p  12256  efgt1p2  12257  efgt1p  12258  sin01gt0  12324  dvds1  12415  3dvds2dec  12428  5ndvds6  12497  bitsmod  12518  bitsinv1lem  12523  isprm5  12715  pcelnn  12895  pockthg  12931  dec5nprm  12988  dec2nprm  12989  modxp1i  12992  2exp8  13009  2exp11  13010  2exp16  13011  2expltfac  13013  ennnfonelemhom  13037  ocndx  13295  ocid  13296  basendxnocndx  13297  plendxnocndx  13298  dsndx  13299  dsid  13300  dsslid  13301  dsndxnn  13302  basendxltdsndx  13303  slotsdifdsndx  13309  unifndx  13310  unifid  13311  unifndxnn  13312  basendxltunifndx  13313  slotsdifunifndx  13316  homndx  13317  homid  13318  homslid  13319  ccondx  13320  ccoid  13321  ccoslid  13322  imasvalstrd  13354  prdsvalstrd  13355  cnfldstr  14574  dveflem  15452  plyid  15472  1sgmprm  15720  perfectlem1  15725  perfectlem2  15726  2lgslem3a  15824  2lgslem3c  15826  edgfid  15859  edgfndx  15860  edgfndxnn  15861  basendxltedgfndx  15863  clwwlkccatlem  16253  umgr2cwwkdifex  16278  1kp2ke3k  16323  ex-exp  16326  ex-fac  16327  012of  16595  isomninnlem  16637  trilpolemisumle  16645  iswomninnlem  16656  iswomni0  16658  ismkvnnlem  16659