Theorem 2timesd 12511

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   + caddc 11159   · cmul 11161  2c2 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-mulcl 11218  ax-mulcom 11220  ax-mulass 11222  ax-distr 11223  ax-1rid 11226  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330

This theorem is referenced by:  lt2addmuld  12518  nn0le2x  12582  fzctr  13681  flhalf  13871  2submod  13974  modaddmodup  13976  m1expeven  14151  expmulnbnd  14275  discr  14280  crre  15154  imval2  15191  abslem2  15379  sqreulem  15399  amgm2  15409  caucvgrlem  15710  iseraltlem2  15720  iseraltlem3  15721  arisum2  15898  fallrisefac  16062  efival  16189  sinadd  16201  cosadd  16202  addsin  16207  subsin  16208  cosmul  16210  addcos  16211  subcos  16212  sin2t  16214  cos2t  16215  eirrlem  16241  sadadd2lem2  16488  pythagtriplem12  16865  pythagtriplem15  16868  pythagtriplem17  16870  difsqpwdvds  16926  prmreclem6  16960  4sqlem11  16994  4sqlem12  16995  vdwlem3  17022  vdwlem8  17027  vdwlem9  17028  vdwlem10  17029  bl2in  24411  tcphcphlem1  25270  nmparlem  25274  cphipval2  25276  minveclem2  25461  minveclem4  25467  ovolunlem1  25533  uniioombllem5  25623  sineq0  26567  cosordlem  26573  tanarg  26662  heron  26882  dcubic1  26889  dquartlem1  26895  quart1lem  26899  sinasin  26933  asinsin  26936  cosasin  26948  efiatan2  26961  2efiatan  26962  atantan  26967  atantayl2  26982  leibpi  26986  log2cnv  26988  lgamgulmlem2  27074  lgamgulmlem3  27075  basellem5  27129  basellem6  27130  ppiub  27249  chtublem  27256  chtub  27257  bcctr  27320  pcbcctr  27321  bcmono  27322  bcmax  27323  bcp1ctr  27324  bposlem1  27329  bposlem2  27330  bposlem9  27337  gausslemma2d  27419  lgsquadlem1  27425  chebbnd1lem2  27515  dchrisumlem2  27535  dchrisum0lem1b  27560  mulog2sumlem1  27579  logdivbnd  27601  selberg3lem1  27602  pntrsumbnd2  27612  selbergr  27613  selberg3r  27614  selberg34r  27616  pntpbnd1a  27630  pntpbnd2  27632  pntlemg  27643  pntlemr  27647  pntlemo  27652  ostth2lem1  27663  ostth3  27683  finsumvtxdg2ssteplem4  29567  nrt2irr  30493  nvge0  30693  minvecolem2  30895  minvecolem4  30900  cdj3lem1  32454  constrrtcc  33777  sqsscirc1  33908  bcprod  35739  unbdqndv2lem1  36511  irrdifflemf  37327  mblfinlem3  37667  ftc1anclem7  37707  areacirclem1  37716  areacirc  37721  isbnd3  37792  lcmineqlem18  42048  aks6d1c7lem1  42182  2xp3dxp2ge1d  42243  sumcubes  42352  3cubeslem2  42701  3cubeslem3r  42703  pellfundex  42902  rmxluc  42953  rmyluc  42954  rmxdbl  42956  rmydbl  42957  jm2.24nn  42976  acongeq  43000  jm2.16nn0  43021  jm3.1lem1  43034  jm3.1lem2  43035  sqrtcval  43659  imo72b2lem0  44183  sineq0ALT  44962  sinmulcos  45885  stirlinglem5  46098  fourierdlem79  46205  fouriercnp  46246  hoicvrrex  46576  2leaddle2  47315  lighneallem4a  47600  gpg5nbgrvtx13starlem2  48033  gpg3kgrtriexlem2  48045  gpg3kgrtriexlem5  48048  nnpw2pmod  48509  itschlc0yqe  48686  sinhpcosh  49314