Theorem 2timesd 12489

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   + caddc 11137   · cmul 11139  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-mulcl 11196  ax-mulcom 11198  ax-mulass 11200  ax-distr 11201  ax-1rid 11204  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308

This theorem is referenced by:  lt2addmuld  12496  nn0le2x  12560  fzctr  13662  flhalf  13852  2submod  13955  modaddmodup  13957  m1expeven  14132  expmulnbnd  14258  discr  14263  crre  15138  imval2  15175  abslem2  15363  sqreulem  15383  amgm2  15393  caucvgrlem  15694  iseraltlem2  15704  iseraltlem3  15705  arisum2  15882  fallrisefac  16046  efival  16175  sinadd  16187  cosadd  16188  addsin  16193  subsin  16194  cosmul  16196  addcos  16197  subcos  16198  sin2t  16200  cos2t  16201  eirrlem  16227  sadadd2lem2  16474  pythagtriplem12  16851  pythagtriplem15  16854  pythagtriplem17  16856  difsqpwdvds  16912  prmreclem6  16946  4sqlem11  16980  4sqlem12  16981  vdwlem3  17008  vdwlem8  17013  vdwlem9  17014  vdwlem10  17015  bl2in  24344  tcphcphlem1  25192  nmparlem  25196  cphipval2  25198  minveclem2  25383  minveclem4  25389  ovolunlem1  25455  uniioombllem5  25545  sineq0  26490  cosordlem  26496  tanarg  26585  heron  26805  dcubic1  26812  dquartlem1  26818  quart1lem  26822  sinasin  26856  asinsin  26859  cosasin  26871  efiatan2  26884  2efiatan  26885  atantan  26890  atantayl2  26905  leibpi  26909  log2cnv  26911  lgamgulmlem2  26997  lgamgulmlem3  26998  basellem5  27052  basellem6  27053  ppiub  27172  chtublem  27179  chtub  27180  bcctr  27243  pcbcctr  27244  bcmono  27245  bcmax  27246  bcp1ctr  27247  bposlem1  27252  bposlem2  27253  bposlem9  27260  gausslemma2d  27342  lgsquadlem1  27348  chebbnd1lem2  27438  dchrisumlem2  27458  dchrisum0lem1b  27483  mulog2sumlem1  27502  logdivbnd  27524  selberg3lem1  27525  pntrsumbnd2  27535  selbergr  27536  selberg3r  27537  selberg34r  27539  pntpbnd1a  27553  pntpbnd2  27555  pntlemg  27566  pntlemr  27570  pntlemo  27575  ostth2lem1  27586  ostth3  27606  finsumvtxdg2ssteplem4  29533  nrt2irr  30459  nvge0  30659  minvecolem2  30861  minvecolem4  30866  cdj3lem1  32420  binom2subadd  32724  constrrtcc  33774  constraddcl  33801  sqsscirc1  33944  bcprod  35760  unbdqndv2lem1  36532  irrdifflemf  37348  mblfinlem3  37688  ftc1anclem7  37728  areacirclem1  37737  areacirc  37742  isbnd3  37813  lcmineqlem18  42064  aks6d1c7lem1  42198  sumcubes  42331  3cubeslem2  42683  3cubeslem3r  42685  pellfundex  42884  rmxluc  42935  rmyluc  42936  rmxdbl  42938  rmydbl  42939  jm2.24nn  42958  acongeq  42982  jm2.16nn0  43003  jm3.1lem1  43016  jm3.1lem2  43017  sqrtcval  43640  imo72b2lem0  44164  sineq0ALT  44936  sinmulcos  45874  stirlinglem5  46087  fourierdlem79  46194  fouriercnp  46235  hoicvrrex  46565  2leaddle2  47307  lighneallem4a  47602  gpg5nbgrvtx13starlem2  48054  gpg3kgrtriexlem2  48066  gpg3kgrtriexlem5  48069  nnpw2pmod  48543  itschlc0yqe  48720  sinhpcosh  49584