Theorem 2timesd 12396

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   + caddc 11041   · cmul 11043  2c2 12212

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulcom 11102  ax-mulass 11104  ax-distr 11105  ax-1rid 11108  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220

This theorem is referenced by:  lt2addmuld  12403  nn0le2x  12467  fzctr  13568  flhalf  13762  2submod  13867  modaddmodup  13869  m1expeven  14044  expmulnbnd  14170  discr  14175  crre  15049  imval2  15086  abslem2  15275  sqreulem  15295  amgm2  15305  caucvgrlem  15608  iseraltlem2  15618  iseraltlem3  15619  arisum2  15796  fallrisefac  15960  efival  16089  sinadd  16101  cosadd  16102  addsin  16107  subsin  16108  cosmul  16110  addcos  16111  subcos  16112  sin2t  16114  cos2t  16115  eirrlem  16141  sadadd2lem2  16389  pythagtriplem12  16766  pythagtriplem15  16769  pythagtriplem17  16771  difsqpwdvds  16827  prmreclem6  16861  4sqlem11  16895  4sqlem12  16896  vdwlem3  16923  vdwlem8  16928  vdwlem9  16929  vdwlem10  16930  bl2in  24356  tcphcphlem1  25203  nmparlem  25207  cphipval2  25209  minveclem2  25394  minveclem4  25400  ovolunlem1  25466  uniioombllem5  25556  sineq0  26501  cosordlem  26507  tanarg  26596  heron  26816  dcubic1  26823  dquartlem1  26829  quart1lem  26833  sinasin  26867  asinsin  26870  cosasin  26882  efiatan2  26895  2efiatan  26896  atantan  26901  atantayl2  26916  leibpi  26920  log2cnv  26922  lgamgulmlem2  27008  lgamgulmlem3  27009  basellem5  27063  basellem6  27064  ppiub  27183  chtublem  27190  chtub  27191  bcctr  27254  pcbcctr  27255  bcmono  27256  bcmax  27257  bcp1ctr  27258  bposlem1  27263  bposlem2  27264  bposlem9  27271  gausslemma2d  27353  lgsquadlem1  27359  chebbnd1lem2  27449  dchrisumlem2  27469  dchrisum0lem1b  27494  mulog2sumlem1  27513  logdivbnd  27535  selberg3lem1  27536  pntrsumbnd2  27546  selbergr  27547  selberg3r  27548  selberg34r  27550  pntpbnd1a  27564  pntpbnd2  27566  pntlemg  27577  pntlemr  27581  pntlemo  27586  ostth2lem1  27597  ostth3  27617  finsumvtxdg2ssteplem4  29634  nrt2irr  30560  nvge0  30761  minvecolem2  30963  minvecolem4  30968  cdj3lem1  32522  binom2subadd  32832  constrrtcc  33913  constraddcl  33940  sqsscirc1  34086  bcprod  35954  unbdqndv2lem1  36731  irrdifflemf  37580  mblfinlem3  37910  ftc1anclem7  37950  areacirclem1  37959  areacirc  37964  isbnd3  38035  lcmineqlem18  42416  aks6d1c7lem1  42550  sumcubes  42683  3cubeslem2  43042  3cubeslem3r  43044  pellfundex  43243  rmxluc  43293  rmyluc  43294  rmxdbl  43296  rmydbl  43297  jm2.24nn  43316  acongeq  43340  jm2.16nn0  43361  jm3.1lem1  43374  jm3.1lem2  43375  sqrtcval  43997  imo72b2lem0  44521  sineq0ALT  45292  sinmulcos  46223  stirlinglem5  46436  fourierdlem79  46543  fouriercnp  46584  hoicvrrex  46914  2leaddle2  47658  modmkpkne  47721  modmknepk  47722  lighneallem4a  47968  gpg5nbgrvtx13starlem2  48432  gpg3kgrtriexlem2  48444  gpg3kgrtriexlem5  48447  nnpw2pmod  48943  itschlc0yqe  49120  sinhpcosh  50099