Theorem 2timesd 12367

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012   · cmul 11014  2c2 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191

This theorem is referenced by:  lt2addmuld  12374  nn0le2x  12438  fzctr  13543  flhalf  13734  2submod  13839  modaddmodup  13841  m1expeven  14016  expmulnbnd  14142  discr  14147  crre  15021  imval2  15058  abslem2  15247  sqreulem  15267  amgm2  15277  caucvgrlem  15580  iseraltlem2  15590  iseraltlem3  15591  arisum2  15768  fallrisefac  15932  efival  16061  sinadd  16073  cosadd  16074  addsin  16079  subsin  16080  cosmul  16082  addcos  16083  subcos  16084  sin2t  16086  cos2t  16087  eirrlem  16113  sadadd2lem2  16361  pythagtriplem12  16738  pythagtriplem15  16741  pythagtriplem17  16743  difsqpwdvds  16799  prmreclem6  16833  4sqlem11  16867  4sqlem12  16868  vdwlem3  16895  vdwlem8  16900  vdwlem9  16901  vdwlem10  16902  bl2in  24286  tcphcphlem1  25133  nmparlem  25137  cphipval2  25139  minveclem2  25324  minveclem4  25330  ovolunlem1  25396  uniioombllem5  25486  sineq0  26431  cosordlem  26437  tanarg  26526  heron  26746  dcubic1  26753  dquartlem1  26759  quart1lem  26763  sinasin  26797  asinsin  26800  cosasin  26812  efiatan2  26825  2efiatan  26826  atantan  26831  atantayl2  26846  leibpi  26850  log2cnv  26852  lgamgulmlem2  26938  lgamgulmlem3  26939  basellem5  26993  basellem6  26994  ppiub  27113  chtublem  27120  chtub  27121  bcctr  27184  pcbcctr  27185  bcmono  27186  bcmax  27187  bcp1ctr  27188  bposlem1  27193  bposlem2  27194  bposlem9  27201  gausslemma2d  27283  lgsquadlem1  27289  chebbnd1lem2  27379  dchrisumlem2  27399  dchrisum0lem1b  27424  mulog2sumlem1  27443  logdivbnd  27465  selberg3lem1  27466  pntrsumbnd2  27476  selbergr  27477  selberg3r  27478  selberg34r  27480  pntpbnd1a  27494  pntpbnd2  27496  pntlemg  27507  pntlemr  27511  pntlemo  27516  ostth2lem1  27527  ostth3  27547  finsumvtxdg2ssteplem4  29494  nrt2irr  30417  nvge0  30617  minvecolem2  30819  minvecolem4  30824  cdj3lem1  32378  binom2subadd  32685  constrrtcc  33702  constraddcl  33729  sqsscirc1  33875  bcprod  35711  unbdqndv2lem1  36483  irrdifflemf  37299  mblfinlem3  37639  ftc1anclem7  37679  areacirclem1  37688  areacirc  37693  isbnd3  37764  lcmineqlem18  42019  aks6d1c7lem1  42153  sumcubes  42286  3cubeslem2  42658  3cubeslem3r  42660  pellfundex  42859  rmxluc  42909  rmyluc  42910  rmxdbl  42912  rmydbl  42913  jm2.24nn  42932  acongeq  42956  jm2.16nn0  42977  jm3.1lem1  42990  jm3.1lem2  42991  sqrtcval  43614  imo72b2lem0  44138  sineq0ALT  44910  sinmulcos  45846  stirlinglem5  46059  fourierdlem79  46166  fouriercnp  46207  hoicvrrex  46537  2leaddle2  47282  modmkpkne  47345  modmknepk  47346  lighneallem4a  47592  gpg5nbgrvtx13starlem2  48056  gpg3kgrtriexlem2  48068  gpg3kgrtriexlem5  48071  nnpw2pmod  48568  itschlc0yqe  48745  sinhpcosh  49725