Theorem 2timesd 11868

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531  2c2 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688

This theorem is referenced by:  lt2addmuld  11875  fzctr  13014  flhalf  13195  2submod  13295  modaddmodup  13297  m1expeven  13472  expmulnbnd  13592  discr  13597  crre  14465  imval2  14502  abslem2  14691  sqreulem  14711  amgm2  14721  caucvgrlem  15021  iseraltlem2  15031  iseraltlem3  15032  arisum2  15208  fallrisefac  15371  efival  15497  sinadd  15509  cosadd  15510  addsin  15515  subsin  15516  cosmul  15518  addcos  15519  subcos  15520  sin2t  15522  cos2t  15523  eirrlem  15549  sadadd2lem2  15789  pythagtriplem12  16153  pythagtriplem15  16156  pythagtriplem17  16158  difsqpwdvds  16213  prmreclem6  16247  4sqlem11  16281  4sqlem12  16282  vdwlem3  16309  vdwlem8  16314  vdwlem9  16315  vdwlem10  16316  bl2in  23007  tcphcphlem1  23839  nmparlem  23843  cphipval2  23845  minveclem2  24030  minveclem4  24036  ovolunlem1  24101  uniioombllem5  24191  sineq0  25116  cosordlem  25122  tanarg  25210  heron  25424  dcubic1  25431  dquartlem1  25437  quart1lem  25441  sinasin  25475  asinsin  25478  cosasin  25490  efiatan2  25503  2efiatan  25504  atantan  25509  atantayl2  25524  leibpi  25528  log2cnv  25530  lgamgulmlem2  25615  lgamgulmlem3  25616  basellem5  25670  basellem6  25671  ppiub  25788  chtublem  25795  chtub  25796  bcctr  25859  pcbcctr  25860  bcmono  25861  bcmax  25862  bcp1ctr  25863  bposlem1  25868  bposlem2  25869  bposlem9  25876  gausslemma2d  25958  lgsquadlem1  25964  chebbnd1lem2  26054  dchrisumlem2  26074  dchrisum0lem1b  26099  mulog2sumlem1  26118  logdivbnd  26140  selberg3lem1  26141  pntrsumbnd2  26151  selbergr  26152  selberg3r  26153  selberg34r  26155  pntpbnd1a  26169  pntpbnd2  26171  pntlemg  26182  pntlemr  26186  pntlemo  26191  ostth2lem1  26202  ostth3  26222  finsumvtxdg2ssteplem4  27338  nvge0  28456  minvecolem2  28658  minvecolem4  28663  cdj3lem1  30217  sqsscirc1  31261  bcprod  33083  unbdqndv2lem1  33961  irrdifflemf  34739  mblfinlem3  35096  ftc1anclem7  35136  areacirclem1  35145  areacirc  35150  isbnd3  35222  lcmineqlem18  39334  2xp3dxp2ge1d  39387  3cubeslem2  39626  3cubeslem3r  39628  pellfundex  39827  rmxluc  39877  rmyluc  39878  rmxdbl  39880  rmydbl  39881  jm2.24nn  39900  acongeq  39924  jm2.16nn0  39945  jm3.1lem1  39958  jm3.1lem2  39959  sqrtcval  40341  imo72b2lem0  40869  sineq0ALT  41643  sinmulcos  42507  stirlinglem5  42720  fourierdlem79  42827  fouriercnp  42868  hoicvrrex  43195  2leaddle2  43855  lighneallem4a  44126  nnpw2pmod  44997  itschlc0yqe  45174  sinhpcosh  45266