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

Theorem 2timesd 9970
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 9859 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2syl 15 1  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756    x. cmul 8758   2c2 9811
This theorem is referenced by:  fzctr  10870  flhalf  10970  expmulnbnd  11249  discr  11254  crre  11615  imval2  11652  abslem2  11839  sqreulem  11859  amgm2  11869  caucvgrlem  12161  iseraltlem2  12171  iseraltlem3  12172  arisum2  12335  efival  12448  sinadd  12460  cosadd  12461  addsin  12466  subsin  12467  cosmul  12469  addcos  12470  subcos  12471  sin2t  12473  cos2t  12474  eirrlem  12498  sadadd2lem2  12657  pythagtriplem12  12895  pythagtriplem15  12898  pythagtriplem17  12900  prmreclem6  12984  4sqlem11  13018  4sqlem12  13019  vdwlem3  13046  vdwlem8  13051  vdwlem9  13052  vdwlem10  13053  bl2in  17973  tchcphlem1  18681  nmparlem  18685  minveclem2  18806  minveclem4  18812  ovolunlem1  18872  uniioombllem5  18958  sineq0  19905  cosordlem  19909  tanarg  19986  dcubic1  20157  dquartlem1  20163  quart1lem  20167  sinasin  20201  asinsin  20204  cosasin  20216  efiatan2  20229  2efiatan  20230  atantan  20235  atantayl2  20250  leibpi  20254  log2cnv  20256  basellem5  20338  basellem6  20339  ppiub  20459  chtublem  20466  chtub  20467  bcctr  20530  pcbcctr  20531  bcmono  20532  bcmax  20533  bcp1ctr  20534  bposlem1  20539  bposlem2  20540  bposlem9  20547  lgsquadlem1  20609  chebbnd1lem2  20635  dchrisumlem2  20655  dchrisum0lem1b  20680  mulog2sumlem1  20699  logdivbnd  20721  selberg3lem1  20722  pntrsumbnd2  20732  selbergr  20733  selberg3r  20734  selberg34r  20736  pntpbnd1a  20750  pntpbnd2  20752  pntlemg  20763  pntlemr  20767  pntlemo  20772  ostth2lem1  20783  ostth3  20803  nvge0  21256  minvecolem2  21470  minvecolem4  21475  cdj3lem1  23030  areacirclem2  25028  areacirc  25034  mslb1  25710  2wsms  25711  isbnd3  26611  pellfundex  27074  rmxluc  27124  rmyluc  27125  rmxdbl  27127  rmydbl  27128  jm2.24nn  27149  acongeq  27173  jm2.16nn0  27200  jm3.1lem1  27213  jm3.1lem2  27214  stirlinglem5  27930  sinhpcosh  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-mulcom 8817  ax-mulass 8819  ax-distr 8820  ax-1rid 8823  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820
  Copyright terms: Public domain W3C validator