Theorem 2timesd 11883

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   + caddc 10542   · cmul 10544  2c2 11695

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-mulcom 10603  ax-mulass 10605  ax-distr 10606  ax-1rid 10609  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-2 11703

This theorem is referenced by:  lt2addmuld  11890  fzctr  13022  flhalf  13203  2submod  13303  modaddmodup  13305  m1expeven  13479  expmulnbnd  13599  discr  13604  crre  14475  imval2  14512  abslem2  14701  sqreulem  14721  amgm2  14731  caucvgrlem  15031  iseraltlem2  15041  iseraltlem3  15042  arisum2  15218  fallrisefac  15381  efival  15507  sinadd  15519  cosadd  15520  addsin  15525  subsin  15526  cosmul  15528  addcos  15529  subcos  15530  sin2t  15532  cos2t  15533  eirrlem  15559  sadadd2lem2  15801  pythagtriplem12  16165  pythagtriplem15  16168  pythagtriplem17  16170  difsqpwdvds  16225  prmreclem6  16259  4sqlem11  16293  4sqlem12  16294  vdwlem3  16321  vdwlem8  16326  vdwlem9  16327  vdwlem10  16328  bl2in  23012  tcphcphlem1  23840  nmparlem  23844  cphipval2  23846  minveclem2  24031  minveclem4  24037  ovolunlem1  24100  uniioombllem5  24190  sineq0  25111  cosordlem  25117  tanarg  25204  heron  25418  dcubic1  25425  dquartlem1  25431  quart1lem  25435  sinasin  25469  asinsin  25472  cosasin  25484  efiatan2  25497  2efiatan  25498  atantan  25503  atantayl2  25518  leibpi  25522  log2cnv  25524  lgamgulmlem2  25609  lgamgulmlem3  25610  basellem5  25664  basellem6  25665  ppiub  25782  chtublem  25789  chtub  25790  bcctr  25853  pcbcctr  25854  bcmono  25855  bcmax  25856  bcp1ctr  25857  bposlem1  25862  bposlem2  25863  bposlem9  25870  gausslemma2d  25952  lgsquadlem1  25958  chebbnd1lem2  26048  dchrisumlem2  26068  dchrisum0lem1b  26093  mulog2sumlem1  26112  logdivbnd  26134  selberg3lem1  26135  pntrsumbnd2  26145  selbergr  26146  selberg3r  26147  selberg34r  26149  pntpbnd1a  26163  pntpbnd2  26165  pntlemg  26176  pntlemr  26180  pntlemo  26185  ostth2lem1  26196  ostth3  26216  finsumvtxdg2ssteplem4  27332  nvge0  28452  minvecolem2  28654  minvecolem4  28659  cdj3lem1  30213  sqsscirc1  31153  bcprod  32972  unbdqndv2lem1  33850  mblfinlem3  34933  ftc1anclem7  34975  areacirclem1  34984  areacirc  34989  isbnd3  35064  2xp3dxp2ge1d  39104  3cubeslem2  39289  3cubeslem3r  39291  pellfundex  39490  rmxluc  39540  rmyluc  39541  rmxdbl  39543  rmydbl  39544  jm2.24nn  39563  acongeq  39587  jm2.16nn0  39608  jm3.1lem1  39621  jm3.1lem2  39622  imo72b2lem0  40523  sineq0ALT  41278  sinmulcos  42153  stirlinglem5  42370  fourierdlem79  42477  fouriercnp  42518  hoicvrrex  42845  2leaddle2  43505  lighneallem4a  43780  nnpw2pmod  44650  itschlc0yqe  44754  sinhpcosh  44846