Theorem 2timesd 12146

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   + caddc 10805   · cmul 10807  2c2 11958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulcom 10866  ax-mulass 10868  ax-distr 10869  ax-1rid 10872  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966

This theorem is referenced by:  lt2addmuld  12153  fzctr  13297  flhalf  13478  2submod  13580  modaddmodup  13582  m1expeven  13758  expmulnbnd  13878  discr  13883  crre  14753  imval2  14790  abslem2  14979  sqreulem  14999  amgm2  15009  caucvgrlem  15312  iseraltlem2  15322  iseraltlem3  15323  arisum2  15501  fallrisefac  15663  efival  15789  sinadd  15801  cosadd  15802  addsin  15807  subsin  15808  cosmul  15810  addcos  15811  subcos  15812  sin2t  15814  cos2t  15815  eirrlem  15841  sadadd2lem2  16085  pythagtriplem12  16455  pythagtriplem15  16458  pythagtriplem17  16460  difsqpwdvds  16516  prmreclem6  16550  4sqlem11  16584  4sqlem12  16585  vdwlem3  16612  vdwlem8  16617  vdwlem9  16618  vdwlem10  16619  bl2in  23461  tcphcphlem1  24304  nmparlem  24308  cphipval2  24310  minveclem2  24495  minveclem4  24501  ovolunlem1  24566  uniioombllem5  24656  sineq0  25585  cosordlem  25591  tanarg  25679  heron  25893  dcubic1  25900  dquartlem1  25906  quart1lem  25910  sinasin  25944  asinsin  25947  cosasin  25959  efiatan2  25972  2efiatan  25973  atantan  25978  atantayl2  25993  leibpi  25997  log2cnv  25999  lgamgulmlem2  26084  lgamgulmlem3  26085  basellem5  26139  basellem6  26140  ppiub  26257  chtublem  26264  chtub  26265  bcctr  26328  pcbcctr  26329  bcmono  26330  bcmax  26331  bcp1ctr  26332  bposlem1  26337  bposlem2  26338  bposlem9  26345  gausslemma2d  26427  lgsquadlem1  26433  chebbnd1lem2  26523  dchrisumlem2  26543  dchrisum0lem1b  26568  mulog2sumlem1  26587  logdivbnd  26609  selberg3lem1  26610  pntrsumbnd2  26620  selbergr  26621  selberg3r  26622  selberg34r  26624  pntpbnd1a  26638  pntpbnd2  26640  pntlemg  26651  pntlemr  26655  pntlemo  26660  ostth2lem1  26671  ostth3  26691  finsumvtxdg2ssteplem4  27818  nvge0  28936  minvecolem2  29138  minvecolem4  29143  cdj3lem1  30697  sqsscirc1  31760  bcprod  33610  unbdqndv2lem1  34616  irrdifflemf  35423  mblfinlem3  35743  ftc1anclem7  35783  areacirclem1  35792  areacirc  35797  isbnd3  35869  lcmineqlem18  39982  2xp3dxp2ge1d  40090  3cubeslem2  40423  3cubeslem3r  40425  pellfundex  40624  rmxluc  40674  rmyluc  40675  rmxdbl  40677  rmydbl  40678  jm2.24nn  40697  acongeq  40721  jm2.16nn0  40742  jm3.1lem1  40755  jm3.1lem2  40756  sqrtcval  41138  imo72b2lem0  41665  sineq0ALT  42446  sinmulcos  43296  stirlinglem5  43509  fourierdlem79  43616  fouriercnp  43657  hoicvrrex  43984  2leaddle2  44678  lighneallem4a  44948  nnpw2pmod  45817  itschlc0yqe  45994  sinhpcosh  46328