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 11023
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 11014 . 2 class 2
2 c1 9881 . . 3 class 1
3 caddc 9883 . . 3 class +
42, 2, 3co 6604 . 2 class (1 + 1)
51, 4wceq 1480 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  11034  0le2  11055  2pos  11056  1p1e2  11078  2p2e4  11088  2times  11089  3p2e5  11104  4p2e6  11106  5p2e7  11109  6p2e8  11113  7p2e9  11116  8p2e10OLD  11118  2nn  11129  1lt2  11138  nneo  11405  6p6e12  11546  7p5e12  11551  8p2e10  11554  8p4e12  11558  9p2e11  11563  9p2e11OLD  11564  9p3e12  11565  5t2e10  11578  eluz2b1  11703  x2times  12072  fztp  12339  fzprval  12343  fztpval  12344  fzo12sn  12492  sqval  12862  fac2  13006  faclbnd4lem1  13020  bcp1m1  13047  hashprg  13122  hashprgOLD  13123  hashge2el2difr  13201  swrds2  13619  iseralt  14349  binom11  14489  climcndslem1  14506  climcndslem2  14507  bpoly1  14707  bpolydiflem  14710  bpoly3  14714  bpoly4  14715  ege2le3  14745  ef4p  14768  efgt1p2  14769  eirrlem  14857  odd2np1lem  14988  opoe  15011  bitsfzolem  15080  isprm3  15320  prmind2  15322  dvdsnprmd  15327  prmgt1  15333  pockthlem  15533  pockthg  15534  prmunb  15542  prmreclem2  15545  4sqlem19  15591  vdwlem12  15620  prmgaplem8  15686  decexp2  15703  2expltfac  15723  gsumpr12val  17203  mulg2  17471  psgnunilem2  17836  efgs1b  18070  efgredlemc  18079  lt6abl  18217  abvtrivd  18761  m2detleiblem2  20353  clmvs2  22802  cphipval  22950  pjthlem1  23116  ovolunlem1a  23171  ovolicc1  23191  vitalilem2  23284  itgcnlem  23462  dveflem  23646  coskpi  24176  ang180lem3  24441  tanatan  24546  cosatan  24548  atantayl2  24565  emcllem7  24628  basellem3  24709  basellem5  24711  basellem8  24714  issqf  24762  ppi2  24796  ppi3  24797  cht2  24798  ppieq0  24802  ppiublem2  24828  chpeq0  24833  chtub  24837  chpub  24845  mersenne  24852  perfectlem2  24855  bcp1ctr  24904  bclbnd  24905  bposlem1  24909  bposlem2  24910  bposlem6  24914  lgslem1  24922  lgsval2lem  24932  lgsdir2lem2  24951  lgsdir2lem3  24952  lgsdirprm  24956  lgseisen  25004  m1lgs  25013  rplogsumlem1  25073  rplogsumlem2  25074  dchrisum0flb  25099  dchrisum0re  25102  mulog2sumlem2  25124  pntrmax  25153  pntpbnd2  25176  pntibndlem2  25180  pntlemg  25187  pntlemr  25191  axlowdimlem4  25725  axlowdimlem13  25734  clwlkclwwlklem2a  26766  1wlkdlem1  26863  upgr3v3e3cycl  26906  upgr4cycl4dv4e  26911  numclwlk2lem2f1o  27093  ex-fl  27158  1p1e2apr1  27176  vc2OLD  27269  ipval2  27408  ip2i  27529  hv2times  27764  pjhthlem1  28096  ho2times  28524  stm1addi  28950  staddi  28951  stadd3i  28953  addltmulALT  29151  subfacp1lem1  30866  subfacp1lem5  30871  subfacp1lem6  30872  sin2h  33028  tan2h  33030  poimirlem25  33063  poimirlem27  33065  itg2addnclem3  33092  pell14qrgapw  36917  rmydioph  37058  rmxdioph  37060  expdiophlem1  37065  expdiophlem2  37066  expdioph  37067  relexp2  37447  stoweidlem14  39535  wallispilem3  39588  wallispi2lem2  39593  fourierswlem  39751  fzosplitpr  40633  perfectALTVlem2  40923  nnsum3primes4  40962  nnsum3primesgbe  40966  difmodm1lt  41602  nnlog2ge0lt1  41649
  Copyright terms: Public domain W3C validator