Theorem 2timesd 12455

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   + caddc 11113   · cmul 11115  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulcom 11174  ax-mulass 11176  ax-distr 11177  ax-1rid 11180  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275

This theorem is referenced by:  lt2addmuld  12462  fzctr  13613  flhalf  13795  2submod  13897  modaddmodup  13899  m1expeven  14075  expmulnbnd  14198  discr  14203  crre  15061  imval2  15098  abslem2  15286  sqreulem  15306  amgm2  15316  caucvgrlem  15619  iseraltlem2  15629  iseraltlem3  15630  arisum2  15807  fallrisefac  15969  efival  16095  sinadd  16107  cosadd  16108  addsin  16113  subsin  16114  cosmul  16116  addcos  16117  subcos  16118  sin2t  16120  cos2t  16121  eirrlem  16147  sadadd2lem2  16391  pythagtriplem12  16759  pythagtriplem15  16762  pythagtriplem17  16764  difsqpwdvds  16820  prmreclem6  16854  4sqlem11  16888  4sqlem12  16889  vdwlem3  16916  vdwlem8  16921  vdwlem9  16922  vdwlem10  16923  bl2in  23906  tcphcphlem1  24752  nmparlem  24756  cphipval2  24758  minveclem2  24943  minveclem4  24949  ovolunlem1  25014  uniioombllem5  25104  sineq0  26033  cosordlem  26039  tanarg  26127  heron  26343  dcubic1  26350  dquartlem1  26356  quart1lem  26360  sinasin  26394  asinsin  26397  cosasin  26409  efiatan2  26422  2efiatan  26423  atantan  26428  atantayl2  26443  leibpi  26447  log2cnv  26449  lgamgulmlem2  26534  lgamgulmlem3  26535  basellem5  26589  basellem6  26590  ppiub  26707  chtublem  26714  chtub  26715  bcctr  26778  pcbcctr  26779  bcmono  26780  bcmax  26781  bcp1ctr  26782  bposlem1  26787  bposlem2  26788  bposlem9  26795  gausslemma2d  26877  lgsquadlem1  26883  chebbnd1lem2  26973  dchrisumlem2  26993  dchrisum0lem1b  27018  mulog2sumlem1  27037  logdivbnd  27059  selberg3lem1  27060  pntrsumbnd2  27070  selbergr  27071  selberg3r  27072  selberg34r  27074  pntpbnd1a  27088  pntpbnd2  27090  pntlemg  27101  pntlemr  27105  pntlemo  27110  ostth2lem1  27121  ostth3  27141  finsumvtxdg2ssteplem4  28805  nrt2irr  29726  nvge0  29926  minvecolem2  30128  minvecolem4  30133  cdj3lem1  31687  sqsscirc1  32888  bcprod  34708  unbdqndv2lem1  35385  irrdifflemf  36206  mblfinlem3  36527  ftc1anclem7  36567  areacirclem1  36576  areacirc  36581  isbnd3  36652  lcmineqlem18  40911  2xp3dxp2ge1d  41022  sumcubes  41211  3cubeslem2  41423  3cubeslem3r  41425  pellfundex  41624  rmxluc  41675  rmyluc  41676  rmxdbl  41678  rmydbl  41679  jm2.24nn  41698  acongeq  41722  jm2.16nn0  41743  jm3.1lem1  41756  jm3.1lem2  41757  sqrtcval  42392  imo72b2lem0  42917  sineq0ALT  43698  sinmulcos  44581  stirlinglem5  44794  fourierdlem79  44901  fouriercnp  44942  hoicvrrex  45272  2leaddle2  46006  lighneallem4a  46276  nnpw2pmod  47269  itschlc0yqe  47446  sinhpcosh  47785