Theorem 2timesd 12384

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029   · cmul 11031  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulcom 11090  ax-mulass 11092  ax-distr 11093  ax-1rid 11096  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208

This theorem is referenced by:  lt2addmuld  12391  nn0le2x  12455  fzctr  13556  flhalf  13750  2submod  13855  modaddmodup  13857  m1expeven  14032  expmulnbnd  14158  discr  14163  crre  15037  imval2  15074  abslem2  15263  sqreulem  15283  amgm2  15293  caucvgrlem  15596  iseraltlem2  15606  iseraltlem3  15607  arisum2  15784  fallrisefac  15948  efival  16077  sinadd  16089  cosadd  16090  addsin  16095  subsin  16096  cosmul  16098  addcos  16099  subcos  16100  sin2t  16102  cos2t  16103  eirrlem  16129  sadadd2lem2  16377  pythagtriplem12  16754  pythagtriplem15  16757  pythagtriplem17  16759  difsqpwdvds  16815  prmreclem6  16849  4sqlem11  16883  4sqlem12  16884  vdwlem3  16911  vdwlem8  16916  vdwlem9  16917  vdwlem10  16918  bl2in  24344  tcphcphlem1  25191  nmparlem  25195  cphipval2  25197  minveclem2  25382  minveclem4  25388  ovolunlem1  25454  uniioombllem5  25544  sineq0  26489  cosordlem  26495  tanarg  26584  heron  26804  dcubic1  26811  dquartlem1  26817  quart1lem  26821  sinasin  26855  asinsin  26858  cosasin  26870  efiatan2  26883  2efiatan  26884  atantan  26889  atantayl2  26904  leibpi  26908  log2cnv  26910  lgamgulmlem2  26996  lgamgulmlem3  26997  basellem5  27051  basellem6  27052  ppiub  27171  chtublem  27178  chtub  27179  bcctr  27242  pcbcctr  27243  bcmono  27244  bcmax  27245  bcp1ctr  27246  bposlem1  27251  bposlem2  27252  bposlem9  27259  gausslemma2d  27341  lgsquadlem1  27347  chebbnd1lem2  27437  dchrisumlem2  27457  dchrisum0lem1b  27482  mulog2sumlem1  27501  logdivbnd  27523  selberg3lem1  27524  pntrsumbnd2  27534  selbergr  27535  selberg3r  27536  selberg34r  27538  pntpbnd1a  27552  pntpbnd2  27554  pntlemg  27565  pntlemr  27569  pntlemo  27574  ostth2lem1  27585  ostth3  27605  finsumvtxdg2ssteplem4  29622  nrt2irr  30548  nvge0  30748  minvecolem2  30950  minvecolem4  30955  cdj3lem1  32509  binom2subadd  32821  constrrtcc  33892  constraddcl  33919  sqsscirc1  34065  bcprod  35932  unbdqndv2lem1  36709  irrdifflemf  37530  mblfinlem3  37860  ftc1anclem7  37900  areacirclem1  37909  areacirc  37914  isbnd3  37985  lcmineqlem18  42300  aks6d1c7lem1  42434  sumcubes  42568  3cubeslem2  42927  3cubeslem3r  42929  pellfundex  43128  rmxluc  43178  rmyluc  43179  rmxdbl  43181  rmydbl  43182  jm2.24nn  43201  acongeq  43225  jm2.16nn0  43246  jm3.1lem1  43259  jm3.1lem2  43260  sqrtcval  43882  imo72b2lem0  44406  sineq0ALT  45177  sinmulcos  46109  stirlinglem5  46322  fourierdlem79  46429  fouriercnp  46470  hoicvrrex  46800  2leaddle2  47544  modmkpkne  47607  modmknepk  47608  lighneallem4a  47854  gpg5nbgrvtx13starlem2  48318  gpg3kgrtriexlem2  48330  gpg3kgrtriexlem5  48333  nnpw2pmod  48829  itschlc0yqe  49006  sinhpcosh  49985