Theorem 2timesd 11152

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818   · cmul 9820  2c2 10947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulcom 9879  ax-mulass 9881  ax-distr 9882  ax-1rid 9885  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956

This theorem is referenced by:  lt2addmuld  11159  fzctr  12320  flhalf  12493  2submod  12593  modaddmodup  12595  m1expeven  12769  expmulnbnd  12858  discr  12863  crre  13702  imval2  13739  abslem2  13927  sqreulem  13947  amgm2  13957  caucvgrlem  14251  iseraltlem2  14261  iseraltlem3  14262  arisum2  14432  fallrisefac  14595  efival  14721  sinadd  14733  cosadd  14734  addsin  14739  subsin  14740  cosmul  14742  addcos  14743  subcos  14744  sin2t  14746  cos2t  14747  eirrlem  14771  sadadd2lem2  15010  pythagtriplem12  15369  pythagtriplem15  15372  pythagtriplem17  15374  difsqpwdvds  15429  prmreclem6  15463  4sqlem11  15497  4sqlem12  15498  vdwlem3  15525  vdwlem8  15530  vdwlem9  15531  vdwlem10  15532  bl2in  22015  tchcphlem1  22842  nmparlem  22846  cphipval2  22848  minveclem2  23005  minveclem4  23011  ovolunlem1  23072  uniioombllem5  23161  sineq0  24077  cosordlem  24081  tanarg  24169  heron  24365  dcubic1  24372  dquartlem1  24378  quart1lem  24382  sinasin  24416  asinsin  24419  cosasin  24431  efiatan2  24444  2efiatan  24445  atantan  24450  atantayl2  24465  leibpi  24469  log2cnv  24471  lgamgulmlem2  24556  lgamgulmlem3  24557  basellem5  24611  basellem6  24612  ppiub  24729  chtublem  24736  chtub  24737  bcctr  24800  pcbcctr  24801  bcmono  24802  bcmax  24803  bcp1ctr  24804  bposlem1  24809  bposlem2  24810  bposlem9  24817  gausslemma2d  24899  lgsquadlem1  24905  chebbnd1lem2  24959  dchrisumlem2  24979  dchrisum0lem1b  25004  mulog2sumlem1  25023  logdivbnd  25045  selberg3lem1  25046  pntrsumbnd2  25056  selbergr  25057  selberg3r  25058  selberg34r  25060  pntpbnd1a  25074  pntpbnd2  25076  pntlemg  25087  pntlemr  25091  pntlemo  25096  ostth2lem1  25107  ostth3  25127  nvge0  26912  minvecolem2  27115  minvecolem4  27120  cdj3lem1  28677  sqsscirc1  29282  bcprod  30877  unbdqndv2lem1  31670  mblfinlem3  32618  ftc1anclem7  32661  areacirclem1  32670  areacirc  32675  isbnd3  32753  pellfundex  36468  rmxluc  36519  rmyluc  36520  rmxdbl  36522  rmydbl  36523  jm2.24nn  36544  acongeq  36568  jm2.16nn0  36589  jm3.1lem1  36602  jm3.1lem2  36603  imo72b2lem0  37487  sineq0ALT  38195  sinmulcos  38748  stirlinglem5  38971  fourierdlem79  39078  fouriercnp  39119  hoicvrrex  39446  lighneallem4a  40063  2leaddle2  40344  nnpw2pmod  42175  sinhpcosh  42280