Theorem 2timesd 12382

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   + caddc 11027   · cmul 11029  2c2 12198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulcom 11088  ax-mulass 11090  ax-distr 11091  ax-1rid 11094  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206

This theorem is referenced by:  lt2addmuld  12389  nn0le2x  12453  fzctr  13554  flhalf  13748  2submod  13853  modaddmodup  13855  m1expeven  14030  expmulnbnd  14156  discr  14161  crre  15035  imval2  15072  abslem2  15261  sqreulem  15281  amgm2  15291  caucvgrlem  15594  iseraltlem2  15604  iseraltlem3  15605  arisum2  15782  fallrisefac  15946  efival  16075  sinadd  16087  cosadd  16088  addsin  16093  subsin  16094  cosmul  16096  addcos  16097  subcos  16098  sin2t  16100  cos2t  16101  eirrlem  16127  sadadd2lem2  16375  pythagtriplem12  16752  pythagtriplem15  16755  pythagtriplem17  16757  difsqpwdvds  16813  prmreclem6  16847  4sqlem11  16881  4sqlem12  16882  vdwlem3  16909  vdwlem8  16914  vdwlem9  16915  vdwlem10  16916  bl2in  24342  tcphcphlem1  25189  nmparlem  25193  cphipval2  25195  minveclem2  25380  minveclem4  25386  ovolunlem1  25452  uniioombllem5  25542  sineq0  26487  cosordlem  26493  tanarg  26582  heron  26802  dcubic1  26809  dquartlem1  26815  quart1lem  26819  sinasin  26853  asinsin  26856  cosasin  26868  efiatan2  26881  2efiatan  26882  atantan  26887  atantayl2  26902  leibpi  26906  log2cnv  26908  lgamgulmlem2  26994  lgamgulmlem3  26995  basellem5  27049  basellem6  27050  ppiub  27169  chtublem  27176  chtub  27177  bcctr  27240  pcbcctr  27241  bcmono  27242  bcmax  27243  bcp1ctr  27244  bposlem1  27249  bposlem2  27250  bposlem9  27257  gausslemma2d  27339  lgsquadlem1  27345  chebbnd1lem2  27435  dchrisumlem2  27455  dchrisum0lem1b  27480  mulog2sumlem1  27499  logdivbnd  27521  selberg3lem1  27522  pntrsumbnd2  27532  selbergr  27533  selberg3r  27534  selberg34r  27536  pntpbnd1a  27550  pntpbnd2  27552  pntlemg  27563  pntlemr  27567  pntlemo  27572  ostth2lem1  27583  ostth3  27603  finsumvtxdg2ssteplem4  29571  nrt2irr  30497  nvge0  30697  minvecolem2  30899  minvecolem4  30904  cdj3lem1  32458  binom2subadd  32770  constrrtcc  33841  constraddcl  33868  sqsscirc1  34014  bcprod  35881  unbdqndv2lem1  36652  irrdifflemf  37469  mblfinlem3  37799  ftc1anclem7  37839  areacirclem1  37848  areacirc  37853  isbnd3  37924  lcmineqlem18  42239  aks6d1c7lem1  42373  sumcubes  42510  3cubeslem2  42869  3cubeslem3r  42871  pellfundex  43070  rmxluc  43120  rmyluc  43121  rmxdbl  43123  rmydbl  43124  jm2.24nn  43143  acongeq  43167  jm2.16nn0  43188  jm3.1lem1  43201  jm3.1lem2  43202  sqrtcval  43824  imo72b2lem0  44348  sineq0ALT  45119  sinmulcos  46051  stirlinglem5  46264  fourierdlem79  46371  fouriercnp  46412  hoicvrrex  46742  2leaddle2  47486  modmkpkne  47549  modmknepk  47550  lighneallem4a  47796  gpg5nbgrvtx13starlem2  48260  gpg3kgrtriexlem2  48272  gpg3kgrtriexlem5  48275  nnpw2pmod  48771  itschlc0yqe  48948  sinhpcosh  49927