Theorem 2nn0 10812

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 10693	. 2 |- 2 e. NN
2	1	nnnn0i 10803	1 |- 2 e. NN0

Syntax hints:   e. wcel 1767   2c2 10585   NN0cn0 10795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-1cn 9550

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537  df-2 10594  df-n0 10796

This theorem is referenced by:  nn0n0n1ge2  10859  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  4fvwrd4  11790  fzo0to42pr  11869  nn0sqcl  12161  sqmul  12199  resqcl  12203  zsqcl  12206  cu2  12234  i3  12237  i4  12238  binom3  12255  bernneq3  12262  expmulnbnd  12266  nn0opthlem1  12316  fac3  12328  faclbnd2  12337  faclbnd4lem1  12339  faclbnd4lem3  12341  faclbnd5  12344  hash2pr  12481  hashtplei  12488  repsw3  12852  swrd2lsw  12853  2swrd2eqwrdeq  12854  abssq  13102  sqabs  13103  iseraltlem2  13468  iseraltlem3  13469  ef4p  13709  efgt1p2  13710  efi4p  13733  ef01bndlem  13780  cos01bnd  13782  xpnnenOLD  13804  oexpneg  13908  bitsinv2  13952  bitsf1ocnv  13953  sadcaddlem  13966  sadadd2lem  13968  pythagtriplem4  14202  iserodd  14218  prmreclem2  14294  prmreclem6  14298  vdwlem7  14364  vdwlem10  14367  vdwlem12  14369  dec2dvds  14408  dec5dvds  14409  decexp2  14420  2exp4  14430  2exp6  14431  2exp8  14432  2exp16  14433  3exp3  14434  2expltfac  14435  5prm  14452  7prm  14454  11prm  14458  13prm  14459  17prm  14460  19prm  14461  23prm  14462  prmlem2  14463  37prm  14464  43prm  14465  83prm  14466  139prm  14467  163prm  14468  317prm  14469  631prm  14470  1259lem1  14471  1259lem2  14472  1259lem3  14473  1259lem4  14474  1259lem5  14475  1259prm  14476  2503lem1  14477  2503lem2  14478  2503lem3  14479  2503prm  14480  4001lem1  14481  4001lem2  14482  4001lem3  14483  4001lem4  14484  4001prm  14485  ressds  14669  prdsvalstr  14708  pmtrprfval  16318  psgnunilem2  16326  efgredleme  16567  lt6abl  16700  mgpds  16953  srads  17632  cnfldstr  18221  setsmsds  20742  tmslem  20748  tnglem  20917  tngds  20925  sqcn  21141  dveflem  22143  iaa  22483  tangtx  22659  efif1olem3  22692  efif1olem4  22693  root1id  22884  mcubic  22934  cubic2  22935  cubic  22936  binom4  22937  dquartlem2  22939  dquart  22940  quart1cl  22941  quart1lem  22942  quart1  22943  quartlem1  22944  quartlem2  22945  atandmcj  22996  bndatandm  23016  atansopn  23019  atantayl3  23026  leibpilem2  23028  leibpi  23029  leibpisum  23030  log2cnv  23031  log2tlbnd  23032  log2ublem2  23034  log2ublem3  23035  log2ub  23036  birthday  23040  basellem3  23112  basellem4  23113  basellem5  23114  basellem8  23117  issqf  23166  ppi3  23201  ppiublem2  23234  chtublem  23242  mersenne  23258  bcmax  23309  bcp1ctr  23310  bclbnd  23311  bpos1  23314  bposlem2  23316  bposlem6  23320  bposlem8  23322  lgslem1  23327  lgsqrlem2  23373  lgseisenlem4  23383  chebbnd1lem3  23412  rplogsumlem2  23426  dchrisumlem2  23431  dchrisum0flblem1  23449  dchrisum0flblem2  23450  dchrisum0flb  23451  selberglem2  23487  pntrmax  23505  pntlemo  23548  trkgstr  23596  ttgplusg  23885  ttgds  23888  eengstr  23987  usgraex2elv  24102  is2wlk  24271  3v3e3cycl1  24348  constr3trllem3  24356  constr3pthlem3  24361  4cycl4v4e  24370  4cycl4dv  24371  clwwlkn2  24479  wwlkext2clwwlk  24507  konigsberg  24691  extwwlkfablem2lem  24780  numclwwlkovf2  24789  numclwwlk2lem1  24807  numclwlk2lem2f  24808  numclwlk2lem2f1o  24810  1kp2ke3k  24872  ipidsq  25327  strlem3a  26875  zlmds  27609  log2le1  27691  coinflippv  28090  kur14lem8  28325  sinccvglem  28541  bpoly2  29424  bpoly3  29425  bpoly4  29426  fsumcube  29427  dvtan  29670  diophin  30338  irrapxlem5  30394  pellexlem2  30398  pell1qrge1  30438  rmspecnonsq  30475  rmspecfund  30477  rmspecpos  30484  rmxypos  30517  jm2.22  30569  jm2.20nn  30571  jm2.27c  30581  rmydioph  30588  rmxdioph  30590  jm3.1  30594  expdiophlem2  30596  frlmpwfi  30678  isnumbasgrplem3  30686  m1expeven  31169  dvdivf  31280  dvdivbd  31281  itgsinexplem1  31299  itgsinexp  31300  stoweidlem1  31329  wallispilem4  31396  wallispilem5  31397  wallispi2lem2  31400  stirlinglem3  31404  stirlinglem5  31406  stirlinglem7  31408  stirlinglem8  31409  stirlinglem10  31411  stirlinglem11  31412  usgra2pthlem1  31848  usgra2pth  31849  pgrple2abl  32055  pgrpgt2nabl  32056  ply1mulgsumlem2  32086  onetansqsecsq  32254  cotsqcscsq  32255