Theorem 2timesd 12420

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

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

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244

This theorem is referenced by:  lt2addmuld  12427  nn0le2x  12491  fzctr  13594  flhalf  13789  2submod  13894  modaddmodup  13896  m1expeven  14071  expmulnbnd  14197  discr  14202  crre  15076  imval2  15113  abslem2  15302  sqreulem  15322  amgm2  15332  caucvgrlem  15635  iseraltlem2  15645  iseraltlem3  15646  arisum2  15826  fallrisefac  15990  efival  16119  sinadd  16131  cosadd  16132  addsin  16137  subsin  16138  cosmul  16140  addcos  16141  subcos  16142  sin2t  16144  cos2t  16145  eirrlem  16171  sadadd2lem2  16419  pythagtriplem12  16797  pythagtriplem15  16800  pythagtriplem17  16802  difsqpwdvds  16858  prmreclem6  16892  4sqlem11  16926  4sqlem12  16927  vdwlem3  16954  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  bl2in  24365  tcphcphlem1  25202  nmparlem  25206  cphipval2  25208  minveclem2  25393  minveclem4  25399  ovolunlem1  25464  uniioombllem5  25554  sineq0  26488  cosordlem  26494  tanarg  26583  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  26993  lgamgulmlem3  26994  basellem5  27048  basellem6  27049  ppiub  27167  chtublem  27174  chtub  27175  bcctr  27238  pcbcctr  27239  bcmono  27240  bcmax  27241  bcp1ctr  27242  bposlem1  27247  bposlem2  27248  bposlem9  27255  gausslemma2d  27337  lgsquadlem1  27343  chebbnd1lem2  27433  dchrisumlem2  27453  dchrisum0lem1b  27478  mulog2sumlem1  27497  logdivbnd  27519  selberg3lem1  27520  pntrsumbnd2  27530  selbergr  27531  selberg3r  27532  selberg34r  27534  pntpbnd1a  27548  pntpbnd2  27550  pntlemg  27561  pntlemr  27565  pntlemo  27570  ostth2lem1  27581  ostth3  27601  finsumvtxdg2ssteplem4  29617  nrt2irr  30543  nvge0  30744  minvecolem2  30946  minvecolem4  30951  cdj3lem1  32505  binom2subadd  32814  constrrtcc  33879  constraddcl  33906  sqsscirc1  34052  bcprod  35920  unbdqndv2lem1  36769  irrdifflemf  37639  mblfinlem3  37980  ftc1anclem7  38020  areacirclem1  38029  areacirc  38034  isbnd3  38105  lcmineqlem18  42485  aks6d1c7lem1  42619  sumcubes  42745  3cubeslem2  43117  3cubeslem3r  43119  pellfundex  43314  rmxluc  43364  rmyluc  43365  rmxdbl  43367  rmydbl  43368  jm2.24nn  43387  acongeq  43411  jm2.16nn0  43432  jm3.1lem1  43445  jm3.1lem2  43446  sqrtcval  44068  imo72b2lem0  44592  sineq0ALT  45363  sinmulcos  46293  stirlinglem5  46506  fourierdlem79  46613  fouriercnp  46654  hoicvrrex  46984  2leaddle2  47746  modmkpkne  47815  modmknepk  47816  lighneallem4a  48071  gpg5nbgrvtx13starlem2  48548  gpg3kgrtriexlem2  48560  gpg3kgrtriexlem5  48563  nnpw2pmod  49059  itschlc0yqe  49236  sinhpcosh  50215