Theorem 2timesd 12401

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047   · cmul 11049  2c2 12217

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 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-mulcom 11108  ax-mulass 11110  ax-distr 11111  ax-1rid 11114  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225

This theorem is referenced by:  lt2addmuld  12408  nn0le2x  12472  fzctr  13577  flhalf  13768  2submod  13873  modaddmodup  13875  m1expeven  14050  expmulnbnd  14176  discr  14181  crre  15056  imval2  15093  abslem2  15282  sqreulem  15302  amgm2  15312  caucvgrlem  15615  iseraltlem2  15625  iseraltlem3  15626  arisum2  15803  fallrisefac  15967  efival  16096  sinadd  16108  cosadd  16109  addsin  16114  subsin  16115  cosmul  16117  addcos  16118  subcos  16119  sin2t  16121  cos2t  16122  eirrlem  16148  sadadd2lem2  16396  pythagtriplem12  16773  pythagtriplem15  16776  pythagtriplem17  16778  difsqpwdvds  16834  prmreclem6  16868  4sqlem11  16902  4sqlem12  16903  vdwlem3  16930  vdwlem8  16935  vdwlem9  16936  vdwlem10  16937  bl2in  24264  tcphcphlem1  25111  nmparlem  25115  cphipval2  25117  minveclem2  25302  minveclem4  25308  ovolunlem1  25374  uniioombllem5  25464  sineq0  26409  cosordlem  26415  tanarg  26504  heron  26724  dcubic1  26731  dquartlem1  26737  quart1lem  26741  sinasin  26775  asinsin  26778  cosasin  26790  efiatan2  26803  2efiatan  26804  atantan  26809  atantayl2  26824  leibpi  26828  log2cnv  26830  lgamgulmlem2  26916  lgamgulmlem3  26917  basellem5  26971  basellem6  26972  ppiub  27091  chtublem  27098  chtub  27099  bcctr  27162  pcbcctr  27163  bcmono  27164  bcmax  27165  bcp1ctr  27166  bposlem1  27171  bposlem2  27172  bposlem9  27179  gausslemma2d  27261  lgsquadlem1  27267  chebbnd1lem2  27357  dchrisumlem2  27377  dchrisum0lem1b  27402  mulog2sumlem1  27421  logdivbnd  27443  selberg3lem1  27444  pntrsumbnd2  27454  selbergr  27455  selberg3r  27456  selberg34r  27458  pntpbnd1a  27472  pntpbnd2  27474  pntlemg  27485  pntlemr  27489  pntlemo  27494  ostth2lem1  27505  ostth3  27525  finsumvtxdg2ssteplem4  29452  nrt2irr  30375  nvge0  30575  minvecolem2  30777  minvecolem4  30782  cdj3lem1  32336  binom2subadd  32638  constrrtcc  33698  constraddcl  33725  sqsscirc1  33871  bcprod  35698  unbdqndv2lem1  36470  irrdifflemf  37286  mblfinlem3  37626  ftc1anclem7  37666  areacirclem1  37675  areacirc  37680  isbnd3  37751  lcmineqlem18  42007  aks6d1c7lem1  42141  sumcubes  42274  3cubeslem2  42646  3cubeslem3r  42648  pellfundex  42847  rmxluc  42898  rmyluc  42899  rmxdbl  42901  rmydbl  42902  jm2.24nn  42921  acongeq  42945  jm2.16nn0  42966  jm3.1lem1  42979  jm3.1lem2  42980  sqrtcval  43603  imo72b2lem0  44127  sineq0ALT  44899  sinmulcos  45836  stirlinglem5  46049  fourierdlem79  46156  fouriercnp  46197  hoicvrrex  46527  2leaddle2  47272  modmkpkne  47335  modmknepk  47336  lighneallem4a  47582  gpg5nbgrvtx13starlem2  48036  gpg3kgrtriexlem2  48048  gpg3kgrtriexlem5  48051  nnpw2pmod  48545  itschlc0yqe  48722  sinhpcosh  49702