Theorem 2timesd 12414

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030   + caddc 11035   · cmul 11037  2c2 12230

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 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulcom 11096  ax-mulass 11098  ax-distr 11099  ax-1rid 11102  ax-cnre 11105

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238

This theorem is referenced by:  lt2addmuld  12421  nn0le2x  12485  fzctr  13588  flhalf  13783  2submod  13888  modaddmodup  13890  m1expeven  14065  expmulnbnd  14191  discr  14196  crre  15070  imval2  15107  abslem2  15296  sqreulem  15316  amgm2  15326  caucvgrlem  15629  iseraltlem2  15639  iseraltlem3  15640  arisum2  15820  fallrisefac  15984  efival  16113  sinadd  16125  cosadd  16126  addsin  16131  subsin  16132  cosmul  16134  addcos  16135  subcos  16136  sin2t  16138  cos2t  16139  eirrlem  16165  sadadd2lem2  16413  pythagtriplem12  16791  pythagtriplem15  16794  pythagtriplem17  16796  difsqpwdvds  16852  prmreclem6  16886  4sqlem11  16920  4sqlem12  16921  vdwlem3  16948  vdwlem8  16953  vdwlem9  16954  vdwlem10  16955  bl2in  24378  tcphcphlem1  25215  nmparlem  25219  cphipval2  25221  minveclem2  25406  minveclem4  25412  ovolunlem1  25477  uniioombllem5  25567  sineq0  26504  cosordlem  26510  tanarg  26599  heron  26818  dcubic1  26825  dquartlem1  26831  quart1lem  26835  sinasin  26869  asinsin  26872  cosasin  26884  efiatan2  26897  2efiatan  26898  atantan  26903  atantayl2  26918  leibpi  26922  log2cnv  26924  lgamgulmlem2  27010  lgamgulmlem3  27011  basellem5  27065  basellem6  27066  ppiub  27184  chtublem  27191  chtub  27192  bcctr  27255  pcbcctr  27256  bcmono  27257  bcmax  27258  bcp1ctr  27259  bposlem1  27264  bposlem2  27265  bposlem9  27272  gausslemma2d  27354  lgsquadlem1  27360  chebbnd1lem2  27450  dchrisumlem2  27470  dchrisum0lem1b  27495  mulog2sumlem1  27514  logdivbnd  27536  selberg3lem1  27537  pntrsumbnd2  27547  selbergr  27548  selberg3r  27549  selberg34r  27551  pntpbnd1a  27565  pntpbnd2  27567  pntlemg  27578  pntlemr  27582  pntlemo  27587  ostth2lem1  27598  ostth3  27618  finsumvtxdg2ssteplem4  29635  nrt2irr  30561  nvge0  30762  minvecolem2  30964  minvecolem4  30969  cdj3lem1  32523  binom2subadd  32832  constrrtcc  33898  constraddcl  33925  sqsscirc1  34071  bcprod  35939  unbdqndv2lem1  36788  irrdifflemf  37658  mblfinlem3  37997  ftc1anclem7  38037  areacirclem1  38046  areacirc  38051  isbnd3  38122  lcmineqlem18  42502  aks6d1c7lem1  42636  sumcubes  42762  3cubeslem2  43134  3cubeslem3r  43136  pellfundex  43335  rmxluc  43385  rmyluc  43386  rmxdbl  43388  rmydbl  43389  jm2.24nn  43408  acongeq  43432  jm2.16nn0  43453  jm3.1lem1  43466  jm3.1lem2  43467  sqrtcval  44089  imo72b2lem0  44613  sineq0ALT  45384  sinmulcos  46314  stirlinglem5  46527  fourierdlem79  46634  fouriercnp  46675  hoicvrrex  47005  2leaddle2  47761  modmkpkne  47830  modmknepk  47831  lighneallem4a  48086  gpg5nbgrvtx13starlem2  48563  gpg3kgrtriexlem2  48575  gpg3kgrtriexlem5  48578  nnpw2pmod  49074  itschlc0yqe  49251  sinhpcosh  50230