Theorem 2timesd 12459

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7390  ℂcc 11066   + caddc 11071   · cmul 11073  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulcom 11132  ax-mulass 11134  ax-distr 11135  ax-1rid 11138  ax-cnre 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6471  df-fv 6523  df-ov 7393  df-2 12275

This theorem is referenced by:  lt2addmuld  12466  nn0le2x  12530  fzctr  13640  flhalf  13835  2submod  13940  modaddmodup  13942  m1expeven  14117  expmulnbnd  14243  discr  14248  crre  15122  imval2  15159  abslem2  15348  sqreulem  15368  amgm2  15378  caucvgrlem  15681  iseraltlem2  15691  iseraltlem3  15692  arisum2  15872  fallrisefac  16036  efival  16165  sinadd  16177  cosadd  16178  addsin  16183  subsin  16184  cosmul  16186  addcos  16187  subcos  16188  sin2t  16190  cos2t  16191  eirrlem  16217  sadadd2lem2  16465  pythagtriplem12  16843  pythagtriplem15  16846  pythagtriplem17  16848  difsqpwdvds  16904  prmreclem6  16938  4sqlem11  16972  4sqlem12  16973  vdwlem3  17000  vdwlem8  17005  vdwlem9  17006  vdwlem10  17007  bl2in  24438  tcphcphlem1  25275  nmparlem  25279  cphipval2  25281  minveclem2  25466  minveclem4  25472  ovolunlem1  25537  uniioombllem5  25627  sineq0  26564  cosordlem  26570  tanarg  26659  heron  26878  dcubic1  26885  dquartlem1  26891  quart1lem  26895  sinasin  26929  asinsin  26932  cosasin  26944  efiatan2  26957  2efiatan  26958  atantan  26963  atantayl2  26978  leibpi  26982  log2cnv  26984  lgamgulmlem2  27069  lgamgulmlem3  27070  basellem5  27124  basellem6  27125  ppiub  27243  chtublem  27250  chtub  27251  bcctr  27314  pcbcctr  27315  bcmono  27316  bcmax  27317  bcp1ctr  27318  bposlem1  27323  bposlem2  27324  bposlem9  27331  gausslemma2d  27413  lgsquadlem1  27419  chebbnd1lem2  27509  dchrisumlem2  27529  dchrisum0lem1b  27554  mulog2sumlem1  27573  logdivbnd  27595  selberg3lem1  27596  pntrsumbnd2  27606  selbergr  27607  selberg3r  27608  selberg34r  27610  pntpbnd1a  27624  pntpbnd2  27626  pntlemg  27637  pntlemr  27641  pntlemo  27646  ostth2lem1  27657  ostth3  27677  finsumvtxdg2ssteplem4  29693  nrt2irr  30619  nvge0  30820  minvecolem2  31022  minvecolem4  31027  cdj3lem1  32581  binom2subadd  32891  constrrtcc  33991  constraddcl  34018  sqsscirc1  34164  bcprod  36041  unbdqndv2lem1  36900  irrdifflemf  37770  mblfinlem3  38111  ftc1anclem7  38151  areacirclem1  38160  areacirc  38165  isbnd3  38236  lcmineqlem18  42616  aks6d1c7lem1  42750  sumcubes  42875  3cubeslem2  43219  3cubeslem3r  43221  pellfundex  43416  rmxluc  43466  rmyluc  43467  rmxdbl  43469  rmydbl  43470  jm2.24nn  43489  acongeq  43513  jm2.16nn0  43534  jm3.1lem1  43547  jm3.1lem2  43548  sqrtcval  44170  imo72b2lem0  44694  sineq0ALT  45465  sinmulcos  46392  stirlinglem5  46605  fourierdlem79  46712  fouriercnp  46753  hoicvrrex  47083  2leaddle2  47845  modmkpkne  47914  modmknepk  47915  lighneallem4a  48170  gpg5nbgrvtx13starlem2  48647  gpg3kgrtriexlem2  48659  gpg3kgrtriexlem5  48662  nnpw2pmod  49158  itschlc0yqe  49335  sinhpcosh  50314