MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2timesd Unicode version

Theorem 2timesd 10144
Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
2timesd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
2timesd  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )

Proof of Theorem 2timesd
StepHypRef Expression
1 2timesd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 2times 10033 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717  (class class class)co 6022   CCcc 8923    + caddc 8928    x. cmul 8930   2c2 9983
This theorem is referenced by:  fzctr  11049  flhalf  11160  expmulnbnd  11440  discr  11445  crre  11848  imval2  11885  abslem2  12072  sqreulem  12092  amgm2  12102  caucvgrlem  12395  iseraltlem2  12405  iseraltlem3  12406  arisum2  12569  efival  12682  sinadd  12694  cosadd  12695  addsin  12700  subsin  12701  cosmul  12703  addcos  12704  subcos  12705  sin2t  12707  cos2t  12708  eirrlem  12732  sadadd2lem2  12891  pythagtriplem12  13129  pythagtriplem15  13132  pythagtriplem17  13134  prmreclem6  13218  4sqlem11  13252  4sqlem12  13253  vdwlem3  13280  vdwlem8  13285  vdwlem9  13286  vdwlem10  13287  bl2in  18333  tchcphlem1  19065  nmparlem  19069  minveclem2  19196  minveclem4  19202  ovolunlem1  19262  uniioombllem5  19348  sineq0  20298  cosordlem  20302  tanarg  20383  dcubic1  20554  dquartlem1  20560  quart1lem  20564  sinasin  20598  asinsin  20601  cosasin  20613  efiatan2  20626  2efiatan  20627  atantan  20632  atantayl2  20647  leibpi  20651  log2cnv  20653  basellem5  20736  basellem6  20737  ppiub  20857  chtublem  20864  chtub  20865  bcctr  20928  pcbcctr  20929  bcmono  20930  bcmax  20931  bcp1ctr  20932  bposlem1  20937  bposlem2  20938  bposlem9  20945  lgsquadlem1  21007  chebbnd1lem2  21033  dchrisumlem2  21053  dchrisum0lem1b  21078  mulog2sumlem1  21097  logdivbnd  21119  selberg3lem1  21120  pntrsumbnd2  21130  selbergr  21131  selberg3r  21132  selberg34r  21134  pntpbnd1a  21148  pntpbnd2  21150  pntlemg  21161  pntlemr  21165  pntlemo  21170  ostth2lem1  21181  ostth3  21201  nvge0  22013  minvecolem2  22227  minvecolem4  22232  cdj3lem1  23787  sqsscirc1  24112  lgamgulmlem2  24595  lgamgulmlem3  24596  m1expevenALT  24686  fallrisefac  25111  areacirclem2  25984  areacirc  25990  isbnd3  26186  pellfundex  26642  rmxluc  26692  rmyluc  26693  rmxdbl  26695  rmydbl  26696  jm2.24nn  26717  acongeq  26741  jm2.16nn0  26768  jm3.1lem1  26781  jm3.1lem2  26782  stirlinglem5  27497  sinhpcosh  27831
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-mulcl 8987  ax-mulcom 8989  ax-mulass 8991  ax-distr 8992  ax-1rid 8995  ax-cnre 8998
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-iota 5360  df-fv 5404  df-ov 6025  df-2 9992
  Copyright terms: Public domain W3C validator