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 11242
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 11233 . 2 class 2
2 c1 10100 . . 3 class 1
3 caddc 10102 . . 3 class +
42, 2, 3co 6801 . 2 class (1 + 1)
51, 4wceq 1620 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  11253  0le2  11274  2pos  11275  1p1e2  11297  2p2e4  11307  2times  11308  3p2e5  11323  4p2e6  11325  5p2e7  11328  6p2e8  11332  7p2e9  11335  8p2e10OLD  11337  2nn  11348  1lt2  11357  nneo  11624  6p6e12  11765  7p5e12  11770  8p2e10  11773  8p4e12  11777  9p2e11  11782  9p2e11OLD  11783  9p3e12  11784  5t2e10  11797  eluz2b1  11923  x2times  12293  fztp  12561  fzprval  12565  fztpval  12566  fzo12sn  12716  fzosplitpr  12742  sqval  13087  fac2  13231  faclbnd4lem1  13245  bcp1m1  13272  hashprg  13345  hashprgOLD  13346  hashge2el2difr  13426  swrds2  13856  iseralt  14585  binom11  14734  climcndslem1  14751  climcndslem2  14752  bpoly1  14952  bpolydiflem  14955  bpoly3  14959  bpoly4  14960  ege2le3  14990  ef4p  15013  efgt1p2  15014  eirrlem  15102  odd2np1lem  15237  opoe  15260  bitsfzolem  15329  isprm3  15569  prmind2  15571  dvdsnprmd  15576  prmgt1  15582  pockthlem  15782  pockthg  15783  prmunb  15791  prmreclem2  15794  4sqlem19  15840  vdwlem12  15869  prmgaplem8  15935  decexp2  15952  2expltfac  15972  gsumpr12val  17454  mulg2  17722  psgnunilem2  18086  efgs1b  18320  efgredlemc  18329  lt6abl  18467  abvtrivd  19013  m2detleiblem2  20607  clmvs2  23065  cphipval  23213  pjthlem1  23379  ovolunlem1a  23435  ovolicc1  23455  vitalilem2  23548  itgcnlem  23726  dveflem  23912  coskpi  24442  ang180lem3  24711  tanatan  24816  cosatan  24818  atantayl2  24835  emcllem7  24898  basellem3  24979  basellem5  24981  basellem8  24984  issqf  25032  ppi2  25066  ppi3  25067  cht2  25068  ppieq0  25072  ppiublem2  25098  chpeq0  25103  chtub  25107  chpub  25115  mersenne  25122  perfectlem2  25125  bcp1ctr  25174  bclbnd  25175  bposlem1  25179  bposlem2  25180  bposlem6  25184  lgslem1  25192  lgsval2lem  25202  lgsdir2lem2  25221  lgsdir2lem3  25222  lgsdirprm  25226  lgseisen  25274  m1lgs  25283  rplogsumlem1  25343  rplogsumlem2  25344  dchrisum0flb  25369  dchrisum0re  25372  mulog2sumlem2  25394  pntrmax  25423  pntpbnd2  25446  pntibndlem2  25450  pntlemg  25457  pntlemr  25461  axlowdimlem4  25995  axlowdimlem13  26004  clwlkclwwlklem2a  27092  1wlkdlem1  27260  upgr3v3e3cycl  27303  upgr4cycl4dv4e  27308  numclwlk2lem2f1o  27511  numclwlk2lem2f1oOLD  27518  ex-fl  27586  1p1e2apr1  27604  vc2OLD  27703  ipval2  27842  ip2i  27963  hv2times  28198  pjhthlem1  28530  ho2times  28958  stm1addi  29384  staddi  29385  stadd3i  29387  addltmulALT  29585  threehalves  29903  subfacp1lem1  31439  subfacp1lem5  31444  subfacp1lem6  31445  sin2h  33681  tan2h  33683  poimirlem25  33716  poimirlem27  33718  itg2addnclem3  33745  pell14qrgapw  37911  rmydioph  38052  rmxdioph  38054  expdiophlem1  38059  expdiophlem2  38060  expdioph  38061  relexp2  38440  stoweidlem14  40703  wallispilem3  40756  wallispi2lem2  40761  fourierswlem  40919  perfectALTVlem2  42110  sbgoldbo  42154  nnsum3primes4  42155  nnsum3primesgbe  42159  difmodm1lt  42796  nnlog2ge0lt1  42839
  Copyright terms: Public domain W3C validator