Theorem 2nn0 10592

Description: 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
2nn0	|- 2 e. NN0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 10475	. 2 |- 2 e. NN
2	1	nnnn0i 10583	1 |- 2 e. NN0

Syntax hints:   e. wcel 1761   2c2 10367   NN0cn0 10575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-1cn 9336

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-om 6476  df-recs 6828  df-rdg 6862  df-nn 10319  df-2 10376  df-n0 10576

This theorem is referenced by:  nn0n0n1ge2  10639  7p6e13  10805  8p3e11  10807  8p5e13  10809  9p3e12  10814  9p4e13  10815  4t3e12  10823  4t4e16  10824  5t3e15  10825  5t5e25  10827  6t3e18  10829  6t5e30  10831  7t3e21  10834  7t4e28  10835  7t5e35  10836  7t6e42  10837  7t7e49  10838  8t3e24  10840  8t4e32  10841  8t5e40  10842  9t3e27  10847  9t4e36  10848  9t8e72  10852  9t9e81  10853  decbin3  10856  4fvwrd4  11529  fzo0to42pr  11612  sqmul  11925  resqcl  11929  zsqcl  11932  cu2  11960  i3  11963  i4  11964  binom3  11981  bernneq3  11988  expmulnbnd  11992  nn0opthlem1  12042  fac3  12054  faclbnd2  12063  faclbnd4lem1  12065  faclbnd4lem3  12067  faclbnd5  12070  hash2pr  12174  hashtplei  12181  repsw3  12547  swrd2lsw  12548  2swrd2eqwrdeq  12549  abssq  12791  sqabs  12792  iseraltlem2  13156  iseraltlem3  13157  ef4p  13393  efgt1p2  13394  efi4p  13417  ef01bndlem  13464  cos01bnd  13466  xpnnenOLD  13488  oexpneg  13591  bitsinv2  13635  bitsf1ocnv  13636  sadcaddlem  13649  sadadd2lem  13651  pythagtriplem4  13882  iserodd  13898  prmreclem2  13974  prmreclem6  13978  vdwlem7  14044  vdwlem10  14047  vdwlem12  14049  dec2dvds  14088  dec5dvds  14089  decexp2  14100  2exp4  14110  2exp6  14111  2exp8  14112  2exp16  14113  3exp3  14114  2expltfac  14115  5prm  14132  7prm  14134  11prm  14138  13prm  14139  17prm  14140  19prm  14141  23prm  14142  prmlem2  14143  37prm  14144  43prm  14145  83prm  14146  139prm  14147  163prm  14148  317prm  14149  631prm  14150  1259lem1  14151  1259lem2  14152  1259lem3  14153  1259lem4  14154  1259lem5  14155  1259prm  14156  2503lem1  14157  2503lem2  14158  2503lem3  14159  2503prm  14160  4001lem1  14161  4001lem2  14162  4001lem3  14163  4001lem4  14164  4001prm  14165  ressds  14348  prdsvalstr  14387  pmtrprfval  15986  psgnunilem2  15994  efgredleme  16233  lt6abl  16364  mgpds  16591  srads  17245  cnfldstr  17720  setsmsds  19951  tmslem  19957  tnglem  20126  tngds  20134  sqcn  20350  dveflem  21351  iaa  21734  tangtx  21910  efif1olem3  21943  efif1olem4  21944  root1id  22135  mcubic  22185  cubic2  22186  cubic  22187  binom4  22188  dquartlem2  22190  dquart  22191  quart1cl  22192  quart1lem  22193  quart1  22194  quartlem1  22195  quartlem2  22196  atandmcj  22247  bndatandm  22267  atansopn  22270  atantayl3  22277  leibpilem2  22279  leibpi  22280  leibpisum  22281  log2cnv  22282  log2tlbnd  22283  log2ublem2  22285  log2ublem3  22286  log2ub  22287  birthday  22291  basellem3  22363  basellem4  22364  basellem5  22365  basellem8  22368  issqf  22417  ppi3  22452  ppiublem2  22485  chtublem  22493  mersenne  22509  bcmax  22560  bcp1ctr  22561  bclbnd  22562  bpos1  22565  bposlem2  22567  bposlem6  22571  bposlem8  22573  lgslem1  22578  lgsqrlem2  22624  lgseisenlem4  22634  chebbnd1lem3  22663  rplogsumlem2  22677  dchrisumlem2  22682  dchrisum0flblem1  22700  dchrisum0flblem2  22701  dchrisum0flb  22702  selberglem2  22738  pntrmax  22756  pntlemo  22799  trkgstr  22848  ttgplusg  23043  ttgds  23046  eengstr  23145  usgraex2elv  23235  is2wlk  23383  3v3e3cycl1  23449  constr3trllem3  23457  constr3pthlem3  23462  4cycl4v4e  23471  4cycl4dv  23472  konigsberg  23527  1kp2ke3k  23572  ipidsq  24027  strlem3a  25575  zlmds  26313  log2le1  26386  coinflippv  26780  kur14lem8  27015  sinccvglem  27230  bpoly2  28113  bpoly3  28114  bpoly4  28115  fsumcube  28116  dvtan  28351  diophin  29020  irrapxlem5  29076  pellexlem2  29080  pell1qrge1  29120  rmspecnonsq  29157  rmspecfund  29159  rmspecpos  29166  rmxypos  29199  nn0sqcl  29241  jm2.22  29253  jm2.20nn  29255  jm2.27c  29265  rmydioph  29272  rmxdioph  29274  jm3.1  29278  expdiophlem2  29280  frlmpwfi  29362  isnumbasgrplem3  29370  m1expeven  29681  itgsinexplem1  29703  itgsinexp  29704  stoweidlem1  29705  wallispilem4  29772  wallispilem5  29773  wallispi2lem2  29776  stirlinglem3  29780  stirlinglem5  29782  stirlinglem7  29784  stirlinglem8  29785  stirlinglem10  29787  stirlinglem11  29788  usgra2pthlem1  30209  usgra2pth  30210  clwwlkn2  30347  wwlkext2clwwlk  30374  extwwlkfablem2lem  30577  numclwwlkovf2  30586  numclwwlk2lem1  30604  numclwlk2lem2f  30605  numclwlk2lem2f1o  30607  pgrple2abel  30668  pgrpgt2nabel  30669  onetansqsecsq  30920  cotsqcscsq  30921