Theorem 2timesd 12216

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874   · cmul 10876  2c2 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-mulcom 10935  ax-mulass 10937  ax-distr 10938  ax-1rid 10941  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-2 12036

This theorem is referenced by:  lt2addmuld  12223  fzctr  13368  flhalf  13550  2submod  13652  modaddmodup  13654  m1expeven  13830  expmulnbnd  13950  discr  13955  crre  14825  imval2  14862  abslem2  15051  sqreulem  15071  amgm2  15081  caucvgrlem  15384  iseraltlem2  15394  iseraltlem3  15395  arisum2  15573  fallrisefac  15735  efival  15861  sinadd  15873  cosadd  15874  addsin  15879  subsin  15880  cosmul  15882  addcos  15883  subcos  15884  sin2t  15886  cos2t  15887  eirrlem  15913  sadadd2lem2  16157  pythagtriplem12  16527  pythagtriplem15  16530  pythagtriplem17  16532  difsqpwdvds  16588  prmreclem6  16622  4sqlem11  16656  4sqlem12  16657  vdwlem3  16684  vdwlem8  16689  vdwlem9  16690  vdwlem10  16691  bl2in  23553  tcphcphlem1  24399  nmparlem  24403  cphipval2  24405  minveclem2  24590  minveclem4  24596  ovolunlem1  24661  uniioombllem5  24751  sineq0  25680  cosordlem  25686  tanarg  25774  heron  25988  dcubic1  25995  dquartlem1  26001  quart1lem  26005  sinasin  26039  asinsin  26042  cosasin  26054  efiatan2  26067  2efiatan  26068  atantan  26073  atantayl2  26088  leibpi  26092  log2cnv  26094  lgamgulmlem2  26179  lgamgulmlem3  26180  basellem5  26234  basellem6  26235  ppiub  26352  chtublem  26359  chtub  26360  bcctr  26423  pcbcctr  26424  bcmono  26425  bcmax  26426  bcp1ctr  26427  bposlem1  26432  bposlem2  26433  bposlem9  26440  gausslemma2d  26522  lgsquadlem1  26528  chebbnd1lem2  26618  dchrisumlem2  26638  dchrisum0lem1b  26663  mulog2sumlem1  26682  logdivbnd  26704  selberg3lem1  26705  pntrsumbnd2  26715  selbergr  26716  selberg3r  26717  selberg34r  26719  pntpbnd1a  26733  pntpbnd2  26735  pntlemg  26746  pntlemr  26750  pntlemo  26755  ostth2lem1  26766  ostth3  26786  finsumvtxdg2ssteplem4  27915  nvge0  29035  minvecolem2  29237  minvecolem4  29242  cdj3lem1  30796  sqsscirc1  31858  bcprod  33704  unbdqndv2lem1  34689  irrdifflemf  35496  mblfinlem3  35816  ftc1anclem7  35856  areacirclem1  35865  areacirc  35870  isbnd3  35942  lcmineqlem18  40054  2xp3dxp2ge1d  40162  3cubeslem2  40507  3cubeslem3r  40509  pellfundex  40708  rmxluc  40758  rmyluc  40759  rmxdbl  40761  rmydbl  40762  jm2.24nn  40781  acongeq  40805  jm2.16nn0  40826  jm3.1lem1  40839  jm3.1lem2  40840  sqrtcval  41249  imo72b2lem0  41776  sineq0ALT  42557  sinmulcos  43406  stirlinglem5  43619  fourierdlem79  43726  fouriercnp  43767  hoicvrrex  44094  2leaddle2  44790  lighneallem4a  45060  nnpw2pmod  45929  itschlc0yqe  46106  sinhpcosh  46442