Theorem 2timesd 12457

Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
2timesd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
2timesd	⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Proof of Theorem 2timesd

Step	Hyp	Ref	Expression
1		2timesd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		2times 12350	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7411  ℂcc 11110   + caddc 11115   · cmul 11117  2c2 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-mulcom 11176  ax-mulass 11178  ax-distr 11179  ax-1rid 11182  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-2 12277

This theorem is referenced by:  lt2addmuld  12464  fzctr  13615  flhalf  13797  2submod  13899  modaddmodup  13901  m1expeven  14077  expmulnbnd  14200  discr  14205  crre  15063  imval2  15100  abslem2  15288  sqreulem  15308  amgm2  15318  caucvgrlem  15621  iseraltlem2  15631  iseraltlem3  15632  arisum2  15809  fallrisefac  15971  efival  16097  sinadd  16109  cosadd  16110  addsin  16115  subsin  16116  cosmul  16118  addcos  16119  subcos  16120  sin2t  16122  cos2t  16123  eirrlem  16149  sadadd2lem2  16393  pythagtriplem12  16761  pythagtriplem15  16764  pythagtriplem17  16766  difsqpwdvds  16822  prmreclem6  16856  4sqlem11  16890  4sqlem12  16891  vdwlem3  16918  vdwlem8  16923  vdwlem9  16924  vdwlem10  16925  bl2in  23913  tcphcphlem1  24759  nmparlem  24763  cphipval2  24765  minveclem2  24950  minveclem4  24956  ovolunlem1  25021  uniioombllem5  25111  sineq0  26040  cosordlem  26046  tanarg  26134  heron  26350  dcubic1  26357  dquartlem1  26363  quart1lem  26367  sinasin  26401  asinsin  26404  cosasin  26416  efiatan2  26429  2efiatan  26430  atantan  26435  atantayl2  26450  leibpi  26454  log2cnv  26456  lgamgulmlem2  26541  lgamgulmlem3  26542  basellem5  26596  basellem6  26597  ppiub  26714  chtublem  26721  chtub  26722  bcctr  26785  pcbcctr  26786  bcmono  26787  bcmax  26788  bcp1ctr  26789  bposlem1  26794  bposlem2  26795  bposlem9  26802  gausslemma2d  26884  lgsquadlem1  26890  chebbnd1lem2  26980  dchrisumlem2  27000  dchrisum0lem1b  27025  mulog2sumlem1  27044  logdivbnd  27066  selberg3lem1  27067  pntrsumbnd2  27077  selbergr  27078  selberg3r  27079  selberg34r  27081  pntpbnd1a  27095  pntpbnd2  27097  pntlemg  27108  pntlemr  27112  pntlemo  27117  ostth2lem1  27128  ostth3  27148  finsumvtxdg2ssteplem4  28843  nrt2irr  29764  nvge0  29964  minvecolem2  30166  minvecolem4  30171  cdj3lem1  31725  sqsscirc1  32957  bcprod  34777  unbdqndv2lem1  35471  irrdifflemf  36292  mblfinlem3  36613  ftc1anclem7  36653  areacirclem1  36662  areacirc  36667  isbnd3  36738  lcmineqlem18  40997  2xp3dxp2ge1d  41108  sumcubes  41293  3cubeslem2  41505  3cubeslem3r  41507  pellfundex  41706  rmxluc  41757  rmyluc  41758  rmxdbl  41760  rmydbl  41761  jm2.24nn  41780  acongeq  41804  jm2.16nn0  41825  jm3.1lem1  41838  jm3.1lem2  41839  sqrtcval  42474  imo72b2lem0  42999  sineq0ALT  43780  sinmulcos  44660  stirlinglem5  44873  fourierdlem79  44980  fouriercnp  45021  hoicvrrex  45351  2leaddle2  46085  lighneallem4a  46355  nnpw2pmod  47347  itschlc0yqe  47524  sinhpcosh  47863