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

Theorem 2timesd 10777
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 10650 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    + caddc 9491    x. cmul 9493   2c2 10581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-mulcl 9550  ax-mulcom 9552  ax-mulass 9554  ax-distr 9555  ax-1rid 9558  ax-cnre 9561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-2 10590
This theorem is referenced by:  fzctr  11780  flhalf  11926  2submod  12012  modaddmodup  12014  expmulnbnd  12262  discr  12267  crre  12906  imval2  12943  abslem2  13131  sqreulem  13151  amgm2  13161  caucvgrlem  13454  iseraltlem2  13464  iseraltlem3  13465  arisum2  13631  efival  13744  sinadd  13756  cosadd  13757  addsin  13762  subsin  13763  cosmul  13765  addcos  13766  subcos  13767  sin2t  13769  cos2t  13770  eirrlem  13794  sadadd2lem2  13955  pythagtriplem12  14205  pythagtriplem15  14208  pythagtriplem17  14210  prmreclem6  14294  4sqlem11  14328  4sqlem12  14329  vdwlem3  14356  vdwlem8  14361  vdwlem9  14362  vdwlem10  14363  bl2in  20638  tchcphlem1  21413  nmparlem  21417  minveclem2  21576  minveclem4  21582  ovolunlem1  21643  uniioombllem5  21731  sineq0  22647  cosordlem  22651  tanarg  22732  heron  22897  dcubic1  22904  dquartlem1  22910  quart1lem  22914  sinasin  22948  asinsin  22951  cosasin  22963  efiatan2  22976  2efiatan  22977  atantan  22982  atantayl2  22997  leibpi  23001  log2cnv  23003  basellem5  23086  basellem6  23087  ppiub  23207  chtublem  23214  chtub  23215  bcctr  23278  pcbcctr  23279  bcmono  23280  bcmax  23281  bcp1ctr  23282  bposlem1  23287  bposlem2  23288  bposlem9  23295  lgsquadlem1  23357  chebbnd1lem2  23383  dchrisumlem2  23403  dchrisum0lem1b  23428  mulog2sumlem1  23447  logdivbnd  23469  selberg3lem1  23470  pntrsumbnd2  23480  selbergr  23481  selberg3r  23482  selberg34r  23484  pntpbnd1a  23498  pntpbnd2  23500  pntlemg  23511  pntlemr  23515  pntlemo  23520  ostth2lem1  23531  ostth3  23551  nvge0  25253  minvecolem2  25467  minvecolem4  25472  cdj3lem1  27029  sqsscirc1  27526  lgamgulmlem2  28212  lgamgulmlem3  28213  m1expevenALT  28303  fallrisefac  28724  mblfinlem3  29630  ftc1anclem7  29673  areacirclem1  29684  areacirc  29689  isbnd3  29883  pellfundex  30426  rmxluc  30476  rmyluc  30477  rmxdbl  30479  rmydbl  30480  jm2.24nn  30501  acongeq  30525  jm2.16nn0  30550  jm3.1lem1  30563  jm3.1lem2  30564  lt2addmuld  31050  sinmulcos  31201  stirlinglem5  31378  fourierdlem79  31486  fouriercnp  31527  2leaddle2  31789  sinhpcosh  32215  sineq0ALT  32817
  Copyright terms: Public domain W3C validator