MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2 Structured version   Visualization version   GIF version

Definition df-2 10757
Description: Define the number 2. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-2 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 10748 . 2 class 2
2 c1 9625 . . 3 class 1
3 caddc 9627 . . 3 class +
42, 2, 3co 6363 . 2 class (1 + 1)
51, 4wceq 1468 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  10768  0le2  10789  2pos  10790  1p1e2  10812  2p2e4  10817  2times  10818  3p2e5  10832  4p2e6  10834  5p2e7  10837  6p2e8  10841  7p2e9  10844  8p2e10  10846  2nn  10857  1lt2  10866  nneo  11109  6p6e12  11192  7p5e12  11194  8p4e12  11198  9p2e11  11203  9p3e12  11204  eluz2b1  11320  x2times  11680  fztp  11950  fzprval  11954  fztpval  11955  fzo12sn  12100  sqval  12448  fac2  12579  faclbnd4lem1  12592  bcp1m1  12619  hashprg  12690  hashge2el2difr  12761  swrds2  13171  iseralt  13911  binom11  14050  climcndslem1  14067  climcndslem2  14068  bpoly1  14264  bpolydiflem  14267  bpoly3  14271  bpoly4  14272  ege2le3  14304  ef4p  14327  efgt1p2  14328  eirrlem  14416  odd2np1lem  14525  bitsfzolem  14569  bitsfzolemOLD  14570  isprm3  14795  prmind2  14797  prmgt1  14805  opoe  14923  pockthlem  15011  pockthg  15012  prmunb  15020  prmreclem2  15023  4sqlem19  15075  vdwlem12  15104  prmgaplem8  15190  decexp2  15209  2expltfac  15224  gsumpr12val  16690  mulg2  16927  psgnunilem2  17297  efgs1b  17547  efgredlemc  17556  lt6abl  17690  abvtrivd  18228  m2detleiblem2  19811  pjthlem1  22550  ovolunlem1a  22608  ovolicc1  22628  vitalilem2  22728  itgcnlem  22908  dveflem  23092  coskpi  23636  ang180lem3  23901  tanatan  24006  cosatan  24008  atantayl2  24025  emcllem7  24088  basellem3  24170  basellem5  24172  basellem8  24175  issqf  24224  ppi2  24258  ppi3  24259  cht2  24260  ppieq0  24264  ppiublem2  24292  chpeq0  24297  chtub  24301  chpub  24309  mersenne  24316  perfectlem2  24319  bcp1ctr  24368  bclbnd  24369  bposlem1  24373  bposlem2  24374  bposlem6  24378  lgslem1  24385  lgsval2lem  24395  lgsdir2lem2  24413  lgsdir2lem3  24414  lgsdirprm  24418  lgseisen  24442  m1lgs  24451  rplogsumlem1  24483  rplogsumlem2  24484  dchrisum0flb  24509  dchrisum0re  24512  mulog2sumlem2  24534  pntrmax  24563  pntpbnd2  24586  pntibndlem2  24590  pntlemg  24597  pntlemr  24601  axlowdimlem4  25136  axlowdimlem13  25145  constr3trllem3  25541  constr3pthlem1  25544  constr3pthlem3  25546  clwlkisclwwlklem2a  25674  vdgr1d  25791  konigsberg  25875  numclwlk2lem2f1o  25993  ex-fl  26057  1p1e2apr1  26064  vc2  26337  ipval2  26506  ip2i  26632  hv2times  26877  pjhthlem1  27207  ho2times  27635  stm1addi  28061  staddi  28062  stadd3i  28064  addltmulALT  28262  subfacp1lem1  30054  subfacp1lem5  30059  subfacp1lem6  30060  sin2h  32168  tan2h  32170  poimirlem25  32203  poimirlem27  32205  itg2addnclem3  32233  pell14qrgapw  35962  rmydioph  36109  rmxdioph  36111  expdiophlem1  36116  expdiophlem2  36117  expdioph  36118  relexp2  36508  stoweidlem14  38310  wallispilem3  38365  wallispi2lem2  38370  fourierswlem  38530  perfectALTVlem2  39364  nnsum3primes4  39403  nnsum3primesgbe  39407  fzosplitpr  39587  clwlkclwwlklem2a  40607  11wlkdlem1  40704  upgr3v3e3cycl  40747  upgr4cycl4dv4e  40752  av-numclwlk2lem2f1o  40935  difmodm1lt  41514  nnlog2ge0lt1  41566
  Copyright terms: Public domain W3C validator