Theorem 2timesd 12536

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   + caddc 11187   · cmul 11189  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulcom 11248  ax-mulass 11250  ax-distr 11251  ax-1rid 11254  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356

This theorem is referenced by:  lt2addmuld  12543  fzctr  13697  flhalf  13881  2submod  13983  modaddmodup  13985  m1expeven  14160  expmulnbnd  14284  discr  14289  crre  15163  imval2  15200  abslem2  15388  sqreulem  15408  amgm2  15418  caucvgrlem  15721  iseraltlem2  15731  iseraltlem3  15732  arisum2  15909  fallrisefac  16073  efival  16200  sinadd  16212  cosadd  16213  addsin  16218  subsin  16219  cosmul  16221  addcos  16222  subcos  16223  sin2t  16225  cos2t  16226  eirrlem  16252  sadadd2lem2  16496  pythagtriplem12  16873  pythagtriplem15  16876  pythagtriplem17  16878  difsqpwdvds  16934  prmreclem6  16968  4sqlem11  17002  4sqlem12  17003  vdwlem3  17030  vdwlem8  17035  vdwlem9  17036  vdwlem10  17037  bl2in  24431  tcphcphlem1  25288  nmparlem  25292  cphipval2  25294  minveclem2  25479  minveclem4  25485  ovolunlem1  25551  uniioombllem5  25641  sineq0  26584  cosordlem  26590  tanarg  26679  heron  26899  dcubic1  26906  dquartlem1  26912  quart1lem  26916  sinasin  26950  asinsin  26953  cosasin  26965  efiatan2  26978  2efiatan  26979  atantan  26984  atantayl2  26999  leibpi  27003  log2cnv  27005  lgamgulmlem2  27091  lgamgulmlem3  27092  basellem5  27146  basellem6  27147  ppiub  27266  chtublem  27273  chtub  27274  bcctr  27337  pcbcctr  27338  bcmono  27339  bcmax  27340  bcp1ctr  27341  bposlem1  27346  bposlem2  27347  bposlem9  27354  gausslemma2d  27436  lgsquadlem1  27442  chebbnd1lem2  27532  dchrisumlem2  27552  dchrisum0lem1b  27577  mulog2sumlem1  27596  logdivbnd  27618  selberg3lem1  27619  pntrsumbnd2  27629  selbergr  27630  selberg3r  27631  selberg34r  27633  pntpbnd1a  27647  pntpbnd2  27649  pntlemg  27660  pntlemr  27664  pntlemo  27669  ostth2lem1  27680  ostth3  27700  finsumvtxdg2ssteplem4  29584  nrt2irr  30505  nvge0  30705  minvecolem2  30907  minvecolem4  30912  cdj3lem1  32466  constrrtcc  33726  sqsscirc1  33854  bcprod  35700  unbdqndv2lem1  36475  irrdifflemf  37291  mblfinlem3  37619  ftc1anclem7  37659  areacirclem1  37668  areacirc  37673  isbnd3  37744  lcmineqlem18  42003  aks6d1c7lem1  42137  2xp3dxp2ge1d  42198  sumcubes  42301  3cubeslem2  42641  3cubeslem3r  42643  pellfundex  42842  rmxluc  42893  rmyluc  42894  rmxdbl  42896  rmydbl  42897  jm2.24nn  42916  acongeq  42940  jm2.16nn0  42961  jm3.1lem1  42974  jm3.1lem2  42975  sqrtcval  43603  imo72b2lem0  44127  sineq0ALT  44908  sinmulcos  45786  stirlinglem5  45999  fourierdlem79  46106  fouriercnp  46147  hoicvrrex  46477  2leaddle2  47213  lighneallem4a  47482  nnpw2pmod  48317  itschlc0yqe  48494  sinhpcosh  48832