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

Theorem 2timesd 10166
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 10055 . 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 1721  (class class class)co 6040   CCcc 8944    + caddc 8949    x. cmul 8951   2c2 10005
This theorem is referenced by:  fzctr  11072  flhalf  11186  expmulnbnd  11466  discr  11471  crre  11874  imval2  11911  abslem2  12098  sqreulem  12118  amgm2  12128  caucvgrlem  12421  iseraltlem2  12431  iseraltlem3  12432  arisum2  12595  efival  12708  sinadd  12720  cosadd  12721  addsin  12726  subsin  12727  cosmul  12729  addcos  12730  subcos  12731  sin2t  12733  cos2t  12734  eirrlem  12758  sadadd2lem2  12917  pythagtriplem12  13155  pythagtriplem15  13158  pythagtriplem17  13160  prmreclem6  13244  4sqlem11  13278  4sqlem12  13279  vdwlem3  13306  vdwlem8  13311  vdwlem9  13312  vdwlem10  13313  bl2in  18383  tchcphlem1  19145  nmparlem  19149  minveclem2  19280  minveclem4  19286  ovolunlem1  19346  uniioombllem5  19432  sineq0  20382  cosordlem  20386  tanarg  20467  dcubic1  20638  dquartlem1  20644  quart1lem  20648  sinasin  20682  asinsin  20685  cosasin  20697  efiatan2  20710  2efiatan  20711  atantan  20716  atantayl2  20731  leibpi  20735  log2cnv  20737  basellem5  20820  basellem6  20821  ppiub  20941  chtublem  20948  chtub  20949  bcctr  21012  pcbcctr  21013  bcmono  21014  bcmax  21015  bcp1ctr  21016  bposlem1  21021  bposlem2  21022  bposlem9  21029  lgsquadlem1  21091  chebbnd1lem2  21117  dchrisumlem2  21137  dchrisum0lem1b  21162  mulog2sumlem1  21181  logdivbnd  21203  selberg3lem1  21204  pntrsumbnd2  21214  selbergr  21215  selberg3r  21216  selberg34r  21218  pntpbnd1a  21232  pntpbnd2  21234  pntlemg  21245  pntlemr  21249  pntlemo  21254  ostth2lem1  21265  ostth3  21285  nvge0  22116  minvecolem2  22330  minvecolem4  22335  cdj3lem1  23890  sqsscirc1  24259  lgamgulmlem2  24767  lgamgulmlem3  24768  m1expevenALT  24858  fallrisefac  25293  mblfinlem2  26144  areacirclem2  26181  areacirc  26187  isbnd3  26383  pellfundex  26839  rmxluc  26889  rmyluc  26890  rmxdbl  26892  rmydbl  26893  jm2.24nn  26914  acongeq  26938  jm2.16nn0  26965  jm3.1lem1  26978  jm3.1lem2  26979  stirlinglem5  27694  sinhpcosh  28197
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulcom 9010  ax-mulass 9012  ax-distr 9013  ax-1rid 9016  ax-cnre 9019
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-2 10014
  Copyright terms: Public domain W3C validator