Theorem 1nn0 9396

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 9132	. 2 |- 1 e. NN
2	1	nnnn0i 9388	1 |- 1 e. NN0

Syntax hints:   e. wcel 2200   1c1 8011   NN0cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-int 3924  df-inn 9122  df-n0 9381

This theorem is referenced by:  peano2nn0  9420  deccl  9603  10nn0  9606  numsucc  9628  numadd  9635  numaddc  9636  11multnc  9656  6p5lem  9658  6p6e12  9662  7p5e12  9665  8p4e12  9670  9p2e11  9675  9p3e12  9676  10p10e20  9683  4t4e16  9687  5t2e10  9688  5t4e20  9690  6t3e18  9693  6t4e24  9694  7t3e21  9698  7t4e28  9699  8t3e24  9704  9t3e27  9711  9t9e81  9717  nn01to3  9824  fz0to3un2pr  10331  elfzom1elp1fzo  10420  fzo0sn0fzo1  10439  fldiv4lem1div2  10539  1tonninf  10675  expn1ap0  10783  nn0expcl  10787  sqval  10831  sq10  10946  nn0opthlem1d  10954  fac2  10965  bccl  11001  hashsng  11032  1elfz0hash  11041  snopiswrd  11094  wrdred1hash  11128  pfx1  11251  s3fv1g  11340  bcxmas  12016  arisum  12025  geoisum1  12046  geoisum1c  12047  cvgratnnlemsumlt  12055  mertenslem2  12063  fprodnn0cl  12139  ege2le3  12198  ef4p  12221  efgt1p2  12222  efgt1p  12223  sin01gt0  12289  dvds1  12380  3dvds2dec  12393  5ndvds6  12462  bitsmod  12483  bitsinv1lem  12488  isprm5  12680  pcelnn  12860  pockthg  12896  dec5nprm  12953  dec2nprm  12954  modxp1i  12957  2exp8  12974  2exp11  12975  2exp16  12976  2expltfac  12978  ennnfonelemhom  13002  ocndx  13260  ocid  13261  basendxnocndx  13262  plendxnocndx  13263  dsndx  13264  dsid  13265  dsslid  13266  dsndxnn  13267  basendxltdsndx  13268  slotsdifdsndx  13274  unifndx  13275  unifid  13276  unifndxnn  13277  basendxltunifndx  13278  slotsdifunifndx  13281  homndx  13282  homid  13283  homslid  13284  ccondx  13285  ccoid  13286  ccoslid  13287  imasvalstrd  13319  prdsvalstrd  13320  cnfldstr  14538  dveflem  15416  plyid  15436  1sgmprm  15684  perfectlem1  15689  perfectlem2  15690  2lgslem3a  15788  2lgslem3c  15790  edgfid  15823  edgfndx  15824  edgfndxnn  15825  basendxltedgfndx  15827  clwwlkccatlem  16143  umgr2cwwkdifex  16167  1kp2ke3k  16171  ex-exp  16174  ex-fac  16175  012of  16444  isomninnlem  16486  trilpolemisumle  16494  iswomninnlem  16505  iswomni0  16507  ismkvnnlem  16508