Theorem 2nn0 10886

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 10767	. 2 |- 2 e. NN
2	1	nnnn0i 10877	1 |- 2 e. NN0

Syntax hints:   e. wcel 1887   2c2 10659   NN0cn0 10869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-1cn 9597

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-nn 10610  df-2 10668  df-n0 10870

This theorem is referenced by:  nn0n0n1ge2  10932  7p6e13  11105  8p3e11  11107  8p5e13  11109  9p3e12  11114  9p4e13  11115  4t3e12  11123  4t4e16  11124  5t3e15  11125  5t5e25  11127  6t3e18  11129  6t5e30  11131  7t3e21  11134  7t4e28  11135  7t5e35  11136  7t6e42  11137  7t7e49  11138  8t3e24  11140  8t4e32  11141  8t5e40  11142  9t3e27  11147  9t4e36  11148  9t8e72  11152  9t9e81  11153  decbin3  11156  2eluzge0  11203  fzo0to42pr  12000  nn0sqcl  12299  sqmul  12338  resqcl  12342  zsqcl  12345  cu2  12373  i3  12376  i4  12377  binom3  12393  expmulnbnd  12404  nn0opthlem1  12454  fac3  12466  faclbnd2  12476  faclbnd4lem1  12478  faclbnd4lem3  12480  hash2pr  12630  hashtplei  12640  s4fv2  12991  repsw3  13026  swrd2lsw  13027  2swrd2eqwrdeq  13028  abssq  13369  sqabs  13370  iseraltlem2  13749  iseraltlem3  13750  bpoly2  14110  bpoly3  14111  bpoly4  14112  fsumcube  14113  ef4p  14167  efgt1p2  14168  efi4p  14191  ef01bndlem  14238  cos01bnd  14240  oexpneg  14368  bitsinv2  14417  bitsf1ocnv  14418  sadcaddlem  14431  sadadd2lem  14433  pythagtriplem4  14769  iserodd  14785  prmreclem2  14861  prmreclem6  14865  vdwlem7  14937  vdwlem10  14940  vdwlem12  14942  dec2dvds  15035  dec5dvds  15036  decexp2  15047  2exp4  15057  2exp6  15058  2exp6OLD  15059  2exp8  15060  2exp16  15061  3exp3  15062  2expltfac  15063  5prm  15080  7prm  15082  11prm  15086  13prm  15087  17prm  15088  19prm  15089  23prm  15090  prmlem2  15091  37prm  15092  43prm  15093  83prm  15094  139prm  15095  163prm  15096  317prm  15097  631prm  15098  1259lem1  15102  1259lem2  15103  1259lem3  15104  1259lem4  15105  1259lem5  15106  1259prm  15107  2503lem1  15108  2503lem2  15109  2503lem3  15110  2503prm  15111  4001lem1  15112  4001lem2  15113  4001lem3  15114  4001lem4  15115  4001prm  15116  ressds  15311  prdsvalstr  15351  pmtrprfval  17128  psgnunilem2  17136  efgredleme  17393  lt6abl  17529  mgpds  17733  srads  18409  cnfldstr  18972  setsmsds  21491  tmslem  21497  tnglem  21648  tngds  21656  sqcn  21906  dveflem  22931  iaa  23281  tangtx  23460  efif1olem3  23493  efif1olem4  23494  root1id  23694  mcubic  23773  cubic2  23774  cubic  23775  binom4  23776  dquartlem2  23778  dquart  23779  quart1cl  23780  quart1lem  23781  quart1  23782  quartlem1  23783  quartlem2  23784  atandmcj  23835  bndatandm  23855  atansopn  23858  atantayl3  23865  leibpilem2  23867  leibpi  23868  leibpisum  23869  log2cnv  23870  log2tlbnd  23871  log2ublem2  23873  log2ublem3  23874  log2ub  23875  log2le1  23876  birthday  23880  basellem3  24009  basellem4  24010  basellem5  24011  basellem8  24014  issqf  24063  ppi3  24098  ppiublem2  24131  chtublem  24139  mersenne  24155  bcmax  24206  bcp1ctr  24207  bclbnd  24208  bpos1  24211  bposlem6  24217  bposlem8  24219  lgslem1  24224  lgsqrlem2  24270  lgseisenlem4  24280  chebbnd1lem3  24309  rplogsumlem2  24323  dchrisumlem2  24328  dchrisum0flblem1  24346  dchrisum0flblem2  24347  dchrisum0flb  24348  selberglem2  24384  pntrmax  24402  pntlemo  24445  trkgstr  24492  ttgplusg  24908  ttgds  24911  eengstr  25010  usgraex2elv  25125  is2wlk  25295  3v3e3cycl1  25372  constr3trllem3  25380  4cycl4v4e  25394  4cycl4dv  25395  clwwlkn2  25503  wwlkext2clwwlk  25531  extwwlkfablem2lem  25803  numclwwlkovf2  25812  numclwwlk2lem1  25830  numclwlk2lem2f  25831  numclwlk2lem2f1o  25833  1kp2ke3k  25896  ipidsq  26349  strlem3a  27905  madjusmdetlem4  28656  zlmds  28768  coinflippv  29316  kur14lem8  29936  sinccvglem  30316  dvtan  31992  diophin  35615  irrapxlem5  35670  pellexlem2  35674  pell1qrge1  35716  jm2.22  35850  jm2.20nn  35852  jm2.27c  35862  rmydioph  35869  rmxdioph  35871  expdiophlem2  35877  frlmpwfi  35956  isnumbasgrplem3  35964  amgm2d  36650  m1expevenOLD  37670  dvdivbd  37795  itgsinexplem1  37830  itgsinexp  37831  stoweidlem1  37861  wallispilem4  37930  wallispilem5  37931  wallispi2lem2  37934  stirlinglem3  37938  stirlinglem5  37940  stirlinglem7  37942  stirlinglem8  37943  stirlinglem10  37945  stirlinglem11  37946  hoiqssbllem2  38445  oexpnegALTV  38806  tgblthelfgott  38908  tgoldbachlt  38909  tgoldbach  38911  proththd  38914  3exp4mod41  38916  41prothprmlem1  38917  pfx2  38953  upgredg  39228  upgr2wlk  39664  usgra2pthlem1  39720  usgra2pth  39721  pgrple2abl  40203  pgrpgt2nabl  40204  ply1mulgsumlem2  40232  logbpw2m1  40431  blenpw2m1  40443  dignn0ehalf  40481  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484  nn0mullong  40489  onetansqsecsq  40534  cotsqcscsq  40535