Theorem 2timesd 12411

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   + caddc 11032   · cmul 11034  2c2 12227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulcom 11093  ax-mulass 11095  ax-distr 11096  ax-1rid 11099  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235

This theorem is referenced by:  lt2addmuld  12418  nn0le2x  12482  fzctr  13585  flhalf  13780  2submod  13885  modaddmodup  13887  m1expeven  14062  expmulnbnd  14188  discr  14193  crre  15067  imval2  15104  abslem2  15293  sqreulem  15313  amgm2  15323  caucvgrlem  15626  iseraltlem2  15636  iseraltlem3  15637  arisum2  15817  fallrisefac  15981  efival  16110  sinadd  16122  cosadd  16123  addsin  16128  subsin  16129  cosmul  16131  addcos  16132  subcos  16133  sin2t  16135  cos2t  16136  eirrlem  16162  sadadd2lem2  16410  pythagtriplem12  16788  pythagtriplem15  16791  pythagtriplem17  16793  difsqpwdvds  16849  prmreclem6  16883  4sqlem11  16917  4sqlem12  16918  vdwlem3  16945  vdwlem8  16950  vdwlem9  16951  vdwlem10  16952  bl2in  24383  tcphcphlem1  25220  nmparlem  25224  cphipval2  25226  minveclem2  25411  minveclem4  25417  ovolunlem1  25482  uniioombllem5  25572  sineq0  26506  cosordlem  26512  tanarg  26601  heron  26820  dcubic1  26827  dquartlem1  26833  quart1lem  26837  sinasin  26871  asinsin  26874  cosasin  26886  efiatan2  26899  2efiatan  26900  atantan  26905  atantayl2  26920  leibpi  26924  log2cnv  26926  lgamgulmlem2  27011  lgamgulmlem3  27012  basellem5  27066  basellem6  27067  ppiub  27185  chtublem  27192  chtub  27193  bcctr  27256  pcbcctr  27257  bcmono  27258  bcmax  27259  bcp1ctr  27260  bposlem1  27265  bposlem2  27266  bposlem9  27273  gausslemma2d  27355  lgsquadlem1  27361  chebbnd1lem2  27451  dchrisumlem2  27471  dchrisum0lem1b  27496  mulog2sumlem1  27515  logdivbnd  27537  selberg3lem1  27538  pntrsumbnd2  27548  selbergr  27549  selberg3r  27550  selberg34r  27552  pntpbnd1a  27566  pntpbnd2  27568  pntlemg  27579  pntlemr  27583  pntlemo  27588  ostth2lem1  27599  ostth3  27619  finsumvtxdg2ssteplem4  29635  nrt2irr  30561  nvge0  30762  minvecolem2  30964  minvecolem4  30969  cdj3lem1  32523  binom2subadd  32833  constrrtcc  33919  constraddcl  33946  sqsscirc1  34092  bcprod  35966  unbdqndv2lem1  36815  irrdifflemf  37685  mblfinlem3  38026  ftc1anclem7  38066  areacirclem1  38075  areacirc  38080  isbnd3  38151  lcmineqlem18  42531  aks6d1c7lem1  42665  sumcubes  42790  3cubeslem2  43134  3cubeslem3r  43136  pellfundex  43331  rmxluc  43381  rmyluc  43382  rmxdbl  43384  rmydbl  43385  jm2.24nn  43404  acongeq  43428  jm2.16nn0  43449  jm3.1lem1  43462  jm3.1lem2  43463  sqrtcval  44085  imo72b2lem0  44609  sineq0ALT  45380  sinmulcos  46308  stirlinglem5  46521  fourierdlem79  46628  fouriercnp  46669  hoicvrrex  46999  2leaddle2  47761  modmkpkne  47830  modmknepk  47831  lighneallem4a  48086  gpg5nbgrvtx13starlem2  48563  gpg3kgrtriexlem2  48575  gpg3kgrtriexlem5  48578  nnpw2pmod  49074  itschlc0yqe  49251  sinhpcosh  50230