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 11064
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 11055 . 2 class 2
2 c1 9922 . . 3 class 1
3 caddc 9924 . . 3 class +
42, 2, 3co 6635 . 2 class (1 + 1)
51, 4wceq 1481 1 wff 2 = (1 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  2re  11075  0le2  11096  2pos  11097  1p1e2  11119  2p2e4  11129  2times  11130  3p2e5  11145  4p2e6  11147  5p2e7  11150  6p2e8  11154  7p2e9  11157  8p2e10OLD  11159  2nn  11170  1lt2  11179  nneo  11446  6p6e12  11587  7p5e12  11592  8p2e10  11595  8p4e12  11599  9p2e11  11604  9p2e11OLD  11605  9p3e12  11606  5t2e10  11619  eluz2b1  11744  x2times  12114  fztp  12382  fzprval  12386  fztpval  12387  fzo12sn  12535  sqval  12905  fac2  13049  faclbnd4lem1  13063  bcp1m1  13090  hashprg  13165  hashprgOLD  13166  hashge2el2difr  13246  swrds2  13666  iseralt  14396  binom11  14545  climcndslem1  14562  climcndslem2  14563  bpoly1  14763  bpolydiflem  14766  bpoly3  14770  bpoly4  14771  ege2le3  14801  ef4p  14824  efgt1p2  14825  eirrlem  14913  odd2np1lem  15045  opoe  15068  bitsfzolem  15137  isprm3  15377  prmind2  15379  dvdsnprmd  15384  prmgt1  15390  pockthlem  15590  pockthg  15591  prmunb  15599  prmreclem2  15602  4sqlem19  15648  vdwlem12  15677  prmgaplem8  15743  decexp2  15760  2expltfac  15780  gsumpr12val  17263  mulg2  17531  psgnunilem2  17896  efgs1b  18130  efgredlemc  18139  lt6abl  18277  abvtrivd  18821  m2detleiblem2  20415  clmvs2  22875  cphipval  23023  pjthlem1  23189  ovolunlem1a  23245  ovolicc1  23265  vitalilem2  23359  itgcnlem  23537  dveflem  23723  coskpi  24253  ang180lem3  24522  tanatan  24627  cosatan  24629  atantayl2  24646  emcllem7  24709  basellem3  24790  basellem5  24792  basellem8  24795  issqf  24843  ppi2  24877  ppi3  24878  cht2  24879  ppieq0  24883  ppiublem2  24909  chpeq0  24914  chtub  24918  chpub  24926  mersenne  24933  perfectlem2  24936  bcp1ctr  24985  bclbnd  24986  bposlem1  24990  bposlem2  24991  bposlem6  24995  lgslem1  25003  lgsval2lem  25013  lgsdir2lem2  25032  lgsdir2lem3  25033  lgsdirprm  25037  lgseisen  25085  m1lgs  25094  rplogsumlem1  25154  rplogsumlem2  25155  dchrisum0flb  25180  dchrisum0re  25183  mulog2sumlem2  25205  pntrmax  25234  pntpbnd2  25257  pntibndlem2  25261  pntlemg  25268  pntlemr  25272  axlowdimlem4  25806  axlowdimlem13  25815  clwlkclwwlklem2a  26880  1wlkdlem1  26977  upgr3v3e3cycl  27020  upgr4cycl4dv4e  27025  numclwlk2lem2f1o  27209  ex-fl  27274  1p1e2apr1  27292  vc2OLD  27393  ipval2  27532  ip2i  27653  hv2times  27888  pjhthlem1  28220  ho2times  28648  stm1addi  29074  staddi  29075  stadd3i  29077  addltmulALT  29275  threehalves  29597  subfacp1lem1  31135  subfacp1lem5  31140  subfacp1lem6  31141  sin2h  33370  tan2h  33372  poimirlem25  33405  poimirlem27  33407  itg2addnclem3  33434  pell14qrgapw  37259  rmydioph  37400  rmxdioph  37402  expdiophlem1  37407  expdiophlem2  37408  expdioph  37409  relexp2  37788  stoweidlem14  39994  wallispilem3  40047  wallispi2lem2  40052  fourierswlem  40210  fzosplitpr  41102  perfectALTVlem2  41396  sbgoldbo  41440  nnsum3primes4  41441  nnsum3primesgbe  41445  difmodm1lt  42082  nnlog2ge0lt1  42125
  Copyright terms: Public domain W3C validator