Theorem 2timesd 12364

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009   · cmul 11011  2c2 12180

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188

This theorem is referenced by:  lt2addmuld  12371  nn0le2x  12435  fzctr  13540  flhalf  13734  2submod  13839  modaddmodup  13841  m1expeven  14016  expmulnbnd  14142  discr  14147  crre  15021  imval2  15058  abslem2  15247  sqreulem  15267  amgm2  15277  caucvgrlem  15580  iseraltlem2  15590  iseraltlem3  15591  arisum2  15768  fallrisefac  15932  efival  16061  sinadd  16073  cosadd  16074  addsin  16079  subsin  16080  cosmul  16082  addcos  16083  subcos  16084  sin2t  16086  cos2t  16087  eirrlem  16113  sadadd2lem2  16361  pythagtriplem12  16738  pythagtriplem15  16741  pythagtriplem17  16743  difsqpwdvds  16799  prmreclem6  16833  4sqlem11  16867  4sqlem12  16868  vdwlem3  16895  vdwlem8  16900  vdwlem9  16901  vdwlem10  16902  bl2in  24315  tcphcphlem1  25162  nmparlem  25166  cphipval2  25168  minveclem2  25353  minveclem4  25359  ovolunlem1  25425  uniioombllem5  25515  sineq0  26460  cosordlem  26466  tanarg  26555  heron  26775  dcubic1  26782  dquartlem1  26788  quart1lem  26792  sinasin  26826  asinsin  26829  cosasin  26841  efiatan2  26854  2efiatan  26855  atantan  26860  atantayl2  26875  leibpi  26879  log2cnv  26881  lgamgulmlem2  26967  lgamgulmlem3  26968  basellem5  27022  basellem6  27023  ppiub  27142  chtublem  27149  chtub  27150  bcctr  27213  pcbcctr  27214  bcmono  27215  bcmax  27216  bcp1ctr  27217  bposlem1  27222  bposlem2  27223  bposlem9  27230  gausslemma2d  27312  lgsquadlem1  27318  chebbnd1lem2  27408  dchrisumlem2  27428  dchrisum0lem1b  27453  mulog2sumlem1  27472  logdivbnd  27494  selberg3lem1  27495  pntrsumbnd2  27505  selbergr  27506  selberg3r  27507  selberg34r  27509  pntpbnd1a  27523  pntpbnd2  27525  pntlemg  27536  pntlemr  27540  pntlemo  27545  ostth2lem1  27556  ostth3  27576  finsumvtxdg2ssteplem4  29527  nrt2irr  30453  nvge0  30653  minvecolem2  30855  minvecolem4  30860  cdj3lem1  32414  binom2subadd  32725  constrrtcc  33748  constraddcl  33775  sqsscirc1  33921  bcprod  35782  unbdqndv2lem1  36551  irrdifflemf  37367  mblfinlem3  37707  ftc1anclem7  37747  areacirclem1  37756  areacirc  37761  isbnd3  37832  lcmineqlem18  42087  aks6d1c7lem1  42221  sumcubes  42354  3cubeslem2  42726  3cubeslem3r  42728  pellfundex  42927  rmxluc  42977  rmyluc  42978  rmxdbl  42980  rmydbl  42981  jm2.24nn  43000  acongeq  43024  jm2.16nn0  43045  jm3.1lem1  43058  jm3.1lem2  43059  sqrtcval  43682  imo72b2lem0  44206  sineq0ALT  44977  sinmulcos  45911  stirlinglem5  46124  fourierdlem79  46231  fouriercnp  46272  hoicvrrex  46602  2leaddle2  47337  modmkpkne  47400  modmknepk  47401  lighneallem4a  47647  gpg5nbgrvtx13starlem2  48111  gpg3kgrtriexlem2  48123  gpg3kgrtriexlem5  48126  nnpw2pmod  48623  itschlc0yqe  48800  sinhpcosh  49780