Theorem 2timesd 12451

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104   + caddc 11109   · cmul 11111  2c2 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulcom 11170  ax-mulass 11172  ax-distr 11173  ax-1rid 11176  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271

This theorem is referenced by:  lt2addmuld  12458  fzctr  13609  flhalf  13791  2submod  13893  modaddmodup  13895  m1expeven  14071  expmulnbnd  14194  discr  14199  crre  15057  imval2  15094  abslem2  15282  sqreulem  15302  amgm2  15312  caucvgrlem  15615  iseraltlem2  15625  iseraltlem3  15626  arisum2  15803  fallrisefac  15965  efival  16091  sinadd  16103  cosadd  16104  addsin  16109  subsin  16110  cosmul  16112  addcos  16113  subcos  16114  sin2t  16116  cos2t  16117  eirrlem  16143  sadadd2lem2  16387  pythagtriplem12  16755  pythagtriplem15  16758  pythagtriplem17  16760  difsqpwdvds  16816  prmreclem6  16850  4sqlem11  16884  4sqlem12  16885  vdwlem3  16912  vdwlem8  16917  vdwlem9  16918  vdwlem10  16919  bl2in  23897  tcphcphlem1  24743  nmparlem  24747  cphipval2  24749  minveclem2  24934  minveclem4  24940  ovolunlem1  25005  uniioombllem5  25095  sineq0  26024  cosordlem  26030  tanarg  26118  heron  26332  dcubic1  26339  dquartlem1  26345  quart1lem  26349  sinasin  26383  asinsin  26386  cosasin  26398  efiatan2  26411  2efiatan  26412  atantan  26417  atantayl2  26432  leibpi  26436  log2cnv  26438  lgamgulmlem2  26523  lgamgulmlem3  26524  basellem5  26578  basellem6  26579  ppiub  26696  chtublem  26703  chtub  26704  bcctr  26767  pcbcctr  26768  bcmono  26769  bcmax  26770  bcp1ctr  26771  bposlem1  26776  bposlem2  26777  bposlem9  26784  gausslemma2d  26866  lgsquadlem1  26872  chebbnd1lem2  26962  dchrisumlem2  26982  dchrisum0lem1b  27007  mulog2sumlem1  27026  logdivbnd  27048  selberg3lem1  27049  pntrsumbnd2  27059  selbergr  27060  selberg3r  27061  selberg34r  27063  pntpbnd1a  27077  pntpbnd2  27079  pntlemg  27090  pntlemr  27094  pntlemo  27099  ostth2lem1  27110  ostth3  27130  finsumvtxdg2ssteplem4  28794  nvge0  29913  minvecolem2  30115  minvecolem4  30120  cdj3lem1  31674  sqsscirc1  32876  bcprod  34696  unbdqndv2lem1  35373  irrdifflemf  36194  mblfinlem3  36515  ftc1anclem7  36555  areacirclem1  36564  areacirc  36569  isbnd3  36640  lcmineqlem18  40899  2xp3dxp2ge1d  41010  sumcubes  41206  3cubeslem2  41408  3cubeslem3r  41410  pellfundex  41609  rmxluc  41660  rmyluc  41661  rmxdbl  41663  rmydbl  41664  jm2.24nn  41683  acongeq  41707  jm2.16nn0  41728  jm3.1lem1  41741  jm3.1lem2  41742  sqrtcval  42377  imo72b2lem0  42902  sineq0ALT  43683  sinmulcos  44567  stirlinglem5  44780  fourierdlem79  44887  fouriercnp  44928  hoicvrrex  45258  2leaddle2  45992  lighneallem4a  46262  nnpw2pmod  47222  itschlc0yqe  47399  sinhpcosh  47738