Theorem 2timesd 12486

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11097   + caddc 11102   · cmul 11104  2c2 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-mulcom 11163  ax-mulass 11165  ax-distr 11166  ax-1rid 11169  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302

This theorem is referenced by:  lt2addmuld  12493  nn0le2x  12557  fzctr  13667  flhalf  13862  2submod  13967  modaddmodup  13969  m1expeven  14144  expmulnbnd  14270  discr  14275  crre  15164  imval2  15201  abslem2  15390  sqreulem  15410  amgm2  15420  caucvgrlem  15723  iseraltlem2  15733  iseraltlem3  15734  arisum2  15914  fallrisefac  16078  efival  16207  sinadd  16219  cosadd  16220  addsin  16225  subsin  16226  cosmul  16228  addcos  16229  subcos  16230  sin2t  16232  cos2t  16233  eirrlem  16259  sadadd2lem2  16507  pythagtriplem12  16885  pythagtriplem15  16888  pythagtriplem17  16890  difsqpwdvds  16946  prmreclem6  16980  4sqlem11  17014  4sqlem12  17015  vdwlem3  17042  vdwlem8  17047  vdwlem9  17048  vdwlem10  17049  bl2in  24525  tcphcphlem1  25362  nmparlem  25366  cphipval2  25368  minveclem2  25553  minveclem4  25559  ovolunlem1  25624  uniioombllem5  25714  sineq0  26654  cosordlem  26660  tanarg  26749  heron  26968  dcubic1  26975  dquartlem1  26981  quart1lem  26985  sinasin  27019  asinsin  27022  cosasin  27034  efiatan2  27047  2efiatan  27048  atantan  27053  atantayl2  27068  leibpi  27072  log2cnv  27074  lgamgulmlem2  27159  lgamgulmlem3  27160  basellem5  27214  basellem6  27215  ppiub  27333  chtublem  27340  chtub  27341  bcctr  27404  pcbcctr  27405  bcmono  27406  bcmax  27407  bcp1ctr  27408  bposlem1  27413  bposlem2  27414  bposlem9  27421  gausslemma2d  27503  lgsquadlem1  27509  chebbnd1lem2  27599  dchrisumlem2  27619  dchrisum0lem1b  27644  mulog2sumlem1  27663  logdivbnd  27685  selberg3lem1  27686  pntrsumbnd2  27696  selbergr  27697  selberg3r  27698  selberg34r  27700  pntpbnd1a  27714  pntpbnd2  27716  pntlemg  27727  pntlemr  27731  pntlemo  27736  ostth2lem1  27747  ostth3  27767  finsumvtxdg2ssteplem4  29838  nrt2irr  30764  nvge0  30965  minvecolem2  31167  minvecolem4  31172  cdj3lem1  32726  binom2subadd  33026  constrrtcc  34069  constraddcl  34096  sqsscirc1  34242  bcprod  36128  unbdqndv2lem1  36986  irrdifflemf  37856  mblfinlem3  38197  ftc1anclem7  38237  areacirclem1  38246  areacirc  38251  isbnd3  38322  lcmineqlem18  42702  aks6d1c7lem1  42836  sumcubes  42963  3cubeslem2  43307  3cubeslem3r  43309  pellfundex  43504  rmxluc  43554  rmyluc  43555  rmxdbl  43557  rmydbl  43558  jm2.24nn  43577  acongeq  43601  jm2.16nn0  43622  jm3.1lem1  43635  jm3.1lem2  43636  sqrtcval  44258  imo72b2lem0  44782  sineq0ALT  45536  sinmulcos  46470  stirlinglem5  46683  fourierdlem79  46790  fouriercnp  46831  hoicvrrex  47161  2leaddle2  47923  modmkpkne  47992  modmknepk  47993  lighneallem4a  48248  gpg5nbgrvtx13starlem2  48725  gpg3kgrtriexlem2  48737  gpg3kgrtriexlem5  48740  nnpw2pmod  49247  itschlc0yqe  49424  sinhpcosh  50402