Theorem 2nn0 10813

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 10694	. 2 |- 2 e. NN
2	1	nnnn0i 10804	1 |- 2 e. NN0

Syntax hints:   e. wcel 1802   2c2 10586   NN0cn0 10796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-1cn 9548

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-om 6682  df-recs 7040  df-rdg 7074  df-nn 10538  df-2 10595  df-n0 10797

This theorem is referenced by:  nn0n0n1ge2  10860  7p6e13  11033  8p3e11  11035  8p5e13  11037  9p3e12  11042  9p4e13  11043  4t3e12  11051  4t4e16  11052  5t3e15  11053  5t5e25  11055  6t3e18  11057  6t5e30  11059  7t3e21  11062  7t4e28  11063  7t5e35  11064  7t6e42  11065  7t7e49  11066  8t3e24  11068  8t4e32  11069  8t5e40  11070  9t3e27  11075  9t4e36  11076  9t8e72  11080  9t9e81  11081  decbin3  11084  2eluzge0  11130  fzo0to42pr  11875  nn0sqcl  12167  sqmul  12205  resqcl  12209  zsqcl  12212  cu2  12240  i3  12243  i4  12244  binom3  12261  expmulnbnd  12272  nn0opthlem1  12322  fac3  12334  faclbnd2  12343  faclbnd4lem1  12345  faclbnd4lem3  12347  hash2pr  12489  hashtplei  12496  repsw3  12863  swrd2lsw  12864  2swrd2eqwrdeq  12865  abssq  13113  sqabs  13114  iseraltlem2  13479  iseraltlem3  13480  ef4p  13720  efgt1p2  13721  efi4p  13744  ef01bndlem  13791  cos01bnd  13793  xpnnenOLD  13815  oexpneg  13921  bitsinv2  13965  bitsf1ocnv  13966  sadcaddlem  13979  sadadd2lem  13981  pythagtriplem4  14215  iserodd  14231  prmreclem2  14307  prmreclem6  14311  vdwlem7  14377  vdwlem10  14380  vdwlem12  14382  dec2dvds  14421  dec5dvds  14422  decexp2  14433  2exp4  14443  2exp6OLD  14444  2exp6  14445  2exp8  14446  2exp16  14447  3exp3  14448  2expltfac  14449  5prm  14466  7prm  14468  11prm  14472  13prm  14473  17prm  14474  19prm  14475  23prm  14476  prmlem2  14477  37prm  14478  43prm  14479  83prm  14480  139prm  14481  163prm  14482  317prm  14483  631prm  14484  1259lem1  14485  1259lem2  14486  1259lem3  14487  1259lem4  14488  1259lem5  14489  1259prm  14490  2503lem1  14491  2503lem2  14492  2503lem3  14493  2503prm  14494  4001lem1  14495  4001lem2  14496  4001lem3  14497  4001lem4  14498  4001prm  14499  ressds  14683  prdsvalstr  14722  pmtrprfval  16381  psgnunilem2  16389  efgredleme  16630  lt6abl  16766  mgpds  17019  srads  17700  cnfldstr  18290  setsmsds  20845  tmslem  20851  tnglem  21020  tngds  21028  sqcn  21244  dveflem  22246  iaa  22586  tangtx  22763  efif1olem3  22796  efif1olem4  22797  root1id  22993  mcubic  23043  cubic2  23044  cubic  23045  binom4  23046  dquartlem2  23048  dquart  23049  quart1cl  23050  quart1lem  23051  quart1  23052  quartlem1  23053  quartlem2  23054  atandmcj  23105  bndatandm  23125  atansopn  23128  atantayl3  23135  leibpilem2  23137  leibpi  23138  leibpisum  23139  log2cnv  23140  log2tlbnd  23141  log2ublem2  23143  log2ublem3  23144  log2ub  23145  birthday  23149  basellem3  23221  basellem4  23222  basellem5  23223  basellem8  23226  issqf  23275  ppi3  23310  ppiublem2  23343  chtublem  23351  mersenne  23367  bcmax  23418  bcp1ctr  23419  bclbnd  23420  bpos1  23423  bposlem6  23429  bposlem8  23431  lgslem1  23436  lgsqrlem2  23482  lgseisenlem4  23492  chebbnd1lem3  23521  rplogsumlem2  23535  dchrisumlem2  23540  dchrisum0flblem1  23558  dchrisum0flblem2  23559  dchrisum0flb  23560  selberglem2  23596  pntrmax  23614  pntlemo  23657  trkgstr  23705  ttgplusg  24046  ttgds  24049  eengstr  24148  usgraex2elv  24263  is2wlk  24432  3v3e3cycl1  24509  constr3trllem3  24517  4cycl4v4e  24531  4cycl4dv  24532  clwwlkn2  24640  wwlkext2clwwlk  24668  extwwlkfablem2lem  24940  numclwwlkovf2  24949  numclwwlk2lem1  24967  numclwlk2lem2f  24968  numclwlk2lem2f1o  24970  1kp2ke3k  25032  ipidsq  25488  strlem3a  27036  zlmds  27811  log2le1  27889  coinflippv  28288  kur14lem8  28523  sinccvglem  28904  bpoly2  29787  bpoly3  29788  bpoly4  29789  fsumcube  29790  dvtan  30033  diophin  30674  irrapxlem5  30730  pellexlem2  30734  pell1qrge1  30774  jm2.22  30905  jm2.20nn  30907  jm2.27c  30917  rmydioph  30924  rmxdioph  30926  expdiophlem2  30932  frlmpwfi  31014  isnumbasgrplem3  31022  m1expeven  31509  dvdivbd  31620  itgsinexplem1  31638  itgsinexp  31639  stoweidlem1  31668  wallispilem4  31735  wallispilem5  31736  wallispi2lem2  31739  stirlinglem3  31743  stirlinglem5  31745  stirlinglem7  31747  stirlinglem8  31748  stirlinglem10  31750  stirlinglem11  31751  usgra2pthlem1  32187  usgra2pth  32188  pgrple2abl  32666  pgrpgt2nabl  32667  ply1mulgsumlem2  32697  onetansqsecsq  32865  cotsqcscsq  32866