Theorem 2timesd 12482

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 12371	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	syl 18	1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   + caddc 11098   · cmul 11100  2c2 12290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-mulcl 11157  ax-mulcom 11159  ax-mulass 11161  ax-distr 11162  ax-1rid 11165  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298

This theorem is referenced by:  lt2addmuld  12489  nn0le2x  12553  fzctr  13664  flhalf  13859  2submod  13964  modaddmodup  13966  m1expeven  14141  expmulnbnd  14267  discr  14272  crre  15161  imval2  15198  abslem2  15387  sqreulem  15407  amgm2  15417  caucvgrlem  15720  iseraltlem2  15730  iseraltlem3  15731  arisum2  15911  fallrisefac  16075  efival  16203  sinadd  16215  cosadd  16216  addsin  16221  subsin  16222  cosmul  16224  addcos  16225  subcos  16226  sin2t  16228  cos2t  16229  eirrlem  16255  sadadd2lem2  16503  pythagtriplem12  16881  pythagtriplem15  16884  pythagtriplem17  16886  difsqpwdvds  16942  prmreclem6  16976  4sqlem11  17010  4sqlem12  17011  vdwlem3  17038  vdwlem8  17043  vdwlem9  17044  vdwlem10  17045  bl2in  24557  tcphcphlem1  25394  nmparlem  25398  cphipval2  25400  minveclem2  25585  minveclem4  25591  ovolunlem1  25656  uniioombllem5  25746  sineq0  26689  cosordlem  26695  tanarg  26784  heron  27003  dcubic1  27010  dquartlem1  27016  quart1lem  27020  sinasin  27054  asinsin  27057  cosasin  27069  efiatan2  27082  2efiatan  27083  atantan  27088  atantayl2  27103  leibpi  27107  log2cnv  27109  lgamgulmlem2  27194  lgamgulmlem3  27195  basellem5  27249  basellem6  27250  ppiub  27368  chtublem  27375  chtub  27376  bcctr  27439  pcbcctr  27440  bcmono  27441  bcmax  27442  bcp1ctr  27443  bposlem1  27448  bposlem2  27449  bposlem9  27456  gausslemma2d  27538  lgsquadlem1  27544  chebbnd1lem2  27634  dchrisumlem2  27654  dchrisum0lem1b  27679  mulog2sumlem1  27698  logdivbnd  27720  selberg3lem1  27721  pntrsumbnd2  27731  selbergr  27732  selberg3r  27733  selberg34r  27735  pntpbnd1a  27749  pntpbnd2  27751  pntlemg  27762  pntlemr  27766  pntlemo  27771  ostth2lem1  27782  ostth3  27802  finsumvtxdg2ssteplem4  29898  nrt2irr  30824  nvge0  31025  minvecolem2  31227  minvecolem4  31232  cdj3lem1  32786  binom2subadd  33086  constrrtcc  34125  constraddcl  34152  sqsscirc1  34298  bcprod  36230  unbdqndv2lem1  37098  irrdifflemf  37969  mblfinlem3  38310  ftc1anclem7  38350  areacirclem1  38359  areacirc  38364  isbnd3  38435  lcmineqlem18  42813  aks6d1c7lem1  42947  sumcubes  43074  3cubeslem2  43416  3cubeslem3r  43418  pellfundex  43613  rmxluc  43663  rmyluc  43664  rmxdbl  43666  rmydbl  43667  jm2.24nn  43686  acongeq  43710  jm2.16nn0  43731  jm3.1lem1  43744  jm3.1lem2  43745  sqrtcval  44367  imo72b2lem0  44891  sineq0ALT  45645  sinmulcos  46579  stirlinglem5  46792  fourierdlem79  46899  fouriercnp  46940  hoicvrrex  47270  2leaddle2  48035  modmkpkne  48104  modmknepk  48105  lighneallem4a  48360  gpg5nbgrvtx13starlem2  48837  gpg3kgrtriexlem2  48849  gpg3kgrtriexlem5  48852  nnpw2pmod  49363  itschlc0yqe  49540  sinhpcosh  50518