Theorem 2nn0 10808

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 10689	. 2 |- 2 e. NN
2	1	nnnn0i 10799	1 |- 2 e. NN0

Syntax hints:   e. wcel 1823   2c2 10581   NN0cn0 10791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-1cn 9539

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532  df-2 10590  df-n0 10792

This theorem is referenced by:  nn0n0n1ge2  10855  7p6e13  11030  8p3e11  11032  8p5e13  11034  9p3e12  11039  9p4e13  11040  4t3e12  11048  4t4e16  11049  5t3e15  11050  5t5e25  11052  6t3e18  11054  6t5e30  11056  7t3e21  11059  7t4e28  11060  7t5e35  11061  7t6e42  11062  7t7e49  11063  8t3e24  11065  8t4e32  11066  8t5e40  11067  9t3e27  11072  9t4e36  11073  9t8e72  11077  9t9e81  11078  decbin3  11081  2eluzge0  11126  fzo0to42pr  11882  nn0sqcl  12175  sqmul  12213  resqcl  12217  zsqcl  12220  cu2  12248  i3  12251  i4  12252  binom3  12269  expmulnbnd  12280  nn0opthlem1  12330  fac3  12342  faclbnd2  12351  faclbnd4lem1  12353  faclbnd4lem3  12355  hash2pr  12499  hashtplei  12506  repsw3  12880  swrd2lsw  12881  2swrd2eqwrdeq  12882  abssq  13221  sqabs  13222  iseraltlem2  13587  iseraltlem3  13588  ef4p  13930  efgt1p2  13931  efi4p  13954  ef01bndlem  14001  cos01bnd  14003  xpnnenOLD  14027  oexpneg  14133  bitsinv2  14177  bitsf1ocnv  14178  sadcaddlem  14191  sadadd2lem  14193  pythagtriplem4  14427  iserodd  14443  prmreclem2  14519  prmreclem6  14523  vdwlem7  14589  vdwlem10  14592  vdwlem12  14594  dec2dvds  14633  dec5dvds  14634  decexp2  14645  2exp4  14655  2exp6  14656  2exp6OLD  14657  2exp8  14658  2exp16  14659  3exp3  14660  2expltfac  14661  5prm  14678  7prm  14680  11prm  14684  13prm  14685  17prm  14686  19prm  14687  23prm  14688  prmlem2  14689  37prm  14690  43prm  14691  83prm  14692  139prm  14693  163prm  14694  317prm  14695  631prm  14696  1259lem1  14697  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  1259prm  14702  2503lem1  14703  2503lem2  14704  2503lem3  14705  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  4001prm  14711  ressds  14902  prdsvalstr  14942  pmtrprfval  16711  psgnunilem2  16719  efgredleme  16960  lt6abl  17096  mgpds  17346  srads  18027  cnfldstr  18617  setsmsds  21145  tmslem  21151  tnglem  21320  tngds  21328  sqcn  21544  dveflem  22546  iaa  22887  tangtx  23064  efif1olem3  23097  efif1olem4  23098  root1id  23296  mcubic  23375  cubic2  23376  cubic  23377  binom4  23378  dquartlem2  23380  dquart  23381  quart1cl  23382  quart1lem  23383  quart1  23384  quartlem1  23385  quartlem2  23386  atandmcj  23437  bndatandm  23457  atansopn  23460  atantayl3  23467  leibpilem2  23469  leibpi  23470  leibpisum  23471  log2cnv  23472  log2tlbnd  23473  log2ublem2  23475  log2ublem3  23476  log2ub  23477  log2le1  23478  birthday  23482  basellem3  23554  basellem4  23555  basellem5  23556  basellem8  23559  issqf  23608  ppi3  23643  ppiublem2  23676  chtublem  23684  mersenne  23700  bcmax  23751  bcp1ctr  23752  bclbnd  23753  bpos1  23756  bposlem6  23762  bposlem8  23764  lgslem1  23769  lgsqrlem2  23815  lgseisenlem4  23825  chebbnd1lem3  23854  rplogsumlem2  23868  dchrisumlem2  23873  dchrisum0flblem1  23891  dchrisum0flblem2  23892  dchrisum0flb  23893  selberglem2  23929  pntrmax  23947  pntlemo  23990  trkgstr  24038  ttgplusg  24383  ttgds  24386  eengstr  24485  usgraex2elv  24600  is2wlk  24769  3v3e3cycl1  24846  constr3trllem3  24854  4cycl4v4e  24868  4cycl4dv  24869  clwwlkn2  24977  wwlkext2clwwlk  25005  extwwlkfablem2lem  25277  numclwwlkovf2  25286  numclwwlk2lem1  25304  numclwlk2lem2f  25305  numclwlk2lem2f1o  25307  1kp2ke3k  25369  ipidsq  25821  strlem3a  27369  zlmds  28179  coinflippv  28686  kur14lem8  28921  sinccvglem  29302  bpoly2  30047  bpoly3  30048  bpoly4  30049  fsumcube  30050  dvtan  30305  diophin  30945  irrapxlem5  31001  pellexlem2  31005  pell1qrge1  31045  jm2.22  31176  jm2.20nn  31178  jm2.27c  31188  rmydioph  31195  rmxdioph  31197  expdiophlem2  31203  frlmpwfi  31287  isnumbasgrplem3  31295  m1expeven  31824  dvdivbd  31959  itgsinexplem1  31991  itgsinexp  31992  stoweidlem1  32022  wallispilem4  32089  wallispilem5  32090  wallispi2lem2  32093  stirlinglem3  32097  stirlinglem5  32099  stirlinglem7  32101  stirlinglem8  32102  stirlinglem10  32104  stirlinglem11  32105  oexpnegALTV  32583  pfx2  32640  usgra2pthlem1  32725  usgra2pth  32726  pgrple2abl  33212  pgrpgt2nabl  33213  ply1mulgsumlem2  33241  logbpw2m1  33442  blenpw2m1  33454  dignn0ehalf  33492  nn0sumshdiglemA  33494  nn0sumshdiglemB  33495  nn0mullong  33500  onetansqsecsq  33545  cotsqcscsq  33546