Theorem 2timesd 11881

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540   · cmul 10542  2c2 11693

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-mulcom 10601  ax-mulass 10603  ax-distr 10604  ax-1rid 10607  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-2 11701

This theorem is referenced by:  lt2addmuld  11888  fzctr  13020  flhalf  13201  2submod  13301  modaddmodup  13303  m1expeven  13477  expmulnbnd  13597  discr  13602  crre  14473  imval2  14510  abslem2  14699  sqreulem  14719  amgm2  14729  caucvgrlem  15029  iseraltlem2  15039  iseraltlem3  15040  arisum2  15216  fallrisefac  15379  efival  15505  sinadd  15517  cosadd  15518  addsin  15523  subsin  15524  cosmul  15526  addcos  15527  subcos  15528  sin2t  15530  cos2t  15531  eirrlem  15557  sadadd2lem2  15799  pythagtriplem12  16163  pythagtriplem15  16166  pythagtriplem17  16168  difsqpwdvds  16223  prmreclem6  16257  4sqlem11  16291  4sqlem12  16292  vdwlem3  16319  vdwlem8  16324  vdwlem9  16325  vdwlem10  16326  bl2in  23010  tcphcphlem1  23838  nmparlem  23842  cphipval2  23844  minveclem2  24029  minveclem4  24035  ovolunlem1  24098  uniioombllem5  24188  sineq0  25109  cosordlem  25115  tanarg  25202  heron  25416  dcubic1  25423  dquartlem1  25429  quart1lem  25433  sinasin  25467  asinsin  25470  cosasin  25482  efiatan2  25495  2efiatan  25496  atantan  25501  atantayl2  25516  leibpi  25520  log2cnv  25522  lgamgulmlem2  25607  lgamgulmlem3  25608  basellem5  25662  basellem6  25663  ppiub  25780  chtublem  25787  chtub  25788  bcctr  25851  pcbcctr  25852  bcmono  25853  bcmax  25854  bcp1ctr  25855  bposlem1  25860  bposlem2  25861  bposlem9  25868  gausslemma2d  25950  lgsquadlem1  25956  chebbnd1lem2  26046  dchrisumlem2  26066  dchrisum0lem1b  26091  mulog2sumlem1  26110  logdivbnd  26132  selberg3lem1  26133  pntrsumbnd2  26143  selbergr  26144  selberg3r  26145  selberg34r  26147  pntpbnd1a  26161  pntpbnd2  26163  pntlemg  26174  pntlemr  26178  pntlemo  26183  ostth2lem1  26194  ostth3  26214  finsumvtxdg2ssteplem4  27330  nvge0  28450  minvecolem2  28652  minvecolem4  28657  cdj3lem1  30211  sqsscirc1  31151  bcprod  32970  unbdqndv2lem1  33848  mblfinlem3  34946  ftc1anclem7  34988  areacirclem1  34997  areacirc  35002  isbnd3  35077  2xp3dxp2ge1d  39117  3cubeslem2  39302  3cubeslem3r  39304  pellfundex  39503  rmxluc  39553  rmyluc  39554  rmxdbl  39556  rmydbl  39557  jm2.24nn  39576  acongeq  39600  jm2.16nn0  39621  jm3.1lem1  39634  jm3.1lem2  39635  imo72b2lem0  40536  sineq0ALT  41291  sinmulcos  42166  stirlinglem5  42383  fourierdlem79  42490  fouriercnp  42531  hoicvrrex  42858  2leaddle2  43518  lighneallem4a  43793  nnpw2pmod  44663  itschlc0yqe  44767  sinhpcosh  44859