Theorem 2timesd 12462

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11114   + caddc 11119   · cmul 11121  2c2 12274

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-mulcl 11178  ax-mulcom 11180  ax-mulass 11182  ax-distr 11183  ax-1rid 11186  ax-cnre 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-2 12282

This theorem is referenced by:  lt2addmuld  12469  fzctr  13620  flhalf  13802  2submod  13904  modaddmodup  13906  m1expeven  14082  expmulnbnd  14205  discr  14210  crre  15068  imval2  15105  abslem2  15293  sqreulem  15313  amgm2  15323  caucvgrlem  15626  iseraltlem2  15636  iseraltlem3  15637  arisum2  15814  fallrisefac  15976  efival  16102  sinadd  16114  cosadd  16115  addsin  16120  subsin  16121  cosmul  16123  addcos  16124  subcos  16125  sin2t  16127  cos2t  16128  eirrlem  16154  sadadd2lem2  16398  pythagtriplem12  16766  pythagtriplem15  16769  pythagtriplem17  16771  difsqpwdvds  16827  prmreclem6  16861  4sqlem11  16895  4sqlem12  16896  vdwlem3  16923  vdwlem8  16928  vdwlem9  16929  vdwlem10  16930  bl2in  24226  tcphcphlem1  25083  nmparlem  25087  cphipval2  25089  minveclem2  25274  minveclem4  25280  ovolunlem1  25346  uniioombllem5  25436  sineq0  26373  cosordlem  26379  tanarg  26467  heron  26684  dcubic1  26691  dquartlem1  26697  quart1lem  26701  sinasin  26735  asinsin  26738  cosasin  26750  efiatan2  26763  2efiatan  26764  atantan  26769  atantayl2  26784  leibpi  26788  log2cnv  26790  lgamgulmlem2  26875  lgamgulmlem3  26876  basellem5  26930  basellem6  26931  ppiub  27050  chtublem  27057  chtub  27058  bcctr  27121  pcbcctr  27122  bcmono  27123  bcmax  27124  bcp1ctr  27125  bposlem1  27130  bposlem2  27131  bposlem9  27138  gausslemma2d  27220  lgsquadlem1  27226  chebbnd1lem2  27316  dchrisumlem2  27336  dchrisum0lem1b  27361  mulog2sumlem1  27380  logdivbnd  27402  selberg3lem1  27403  pntrsumbnd2  27413  selbergr  27414  selberg3r  27415  selberg34r  27417  pntpbnd1a  27431  pntpbnd2  27433  pntlemg  27444  pntlemr  27448  pntlemo  27453  ostth2lem1  27464  ostth3  27484  finsumvtxdg2ssteplem4  29238  nrt2irr  30159  nvge0  30359  minvecolem2  30561  minvecolem4  30566  cdj3lem1  32120  sqsscirc1  33352  bcprod  35178  unbdqndv2lem1  35849  irrdifflemf  36670  mblfinlem3  36991  ftc1anclem7  37031  areacirclem1  37040  areacirc  37045  isbnd3  37116  lcmineqlem18  41378  2xp3dxp2ge1d  41489  sumcubes  41674  3cubeslem2  41886  3cubeslem3r  41888  pellfundex  42087  rmxluc  42138  rmyluc  42139  rmxdbl  42141  rmydbl  42142  jm2.24nn  42161  acongeq  42185  jm2.16nn0  42206  jm3.1lem1  42219  jm3.1lem2  42220  sqrtcval  42855  imo72b2lem0  43380  sineq0ALT  44161  sinmulcos  45040  stirlinglem5  45253  fourierdlem79  45360  fouriercnp  45401  hoicvrrex  45731  2leaddle2  46465  lighneallem4a  46735  nnpw2pmod  47431  itschlc0yqe  47608  sinhpcosh  47947