Theorem 2timesd 12502

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   + caddc 11118   · cmul 11120  2c2 12310

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-mulcl 11177  ax-mulcom 11179  ax-mulass 11181  ax-distr 11182  ax-1rid 11185  ax-cnre 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12318

This theorem is used by:  lt2addmuld  12509  nn0le2x  12573  fzctr  13685  flhalf  13881  2submod  13986  modaddmodup  13988  m1expeven  14163  expmulnbnd  14289  discr  14294  crre  15189  imval2  15226  abslem2  15415  sqreulem  15435  amgm2  15445  caucvgrlem  15748  iseraltlem2  15758  iseraltlem3  15759  arisum2  15938  fallrisefac  16102  efival  16230  sinadd  16242  cosadd  16243  addsin  16248  subsin  16249  cosmul  16251  addcos  16252  subcos  16253  sin2t  16255  cos2t  16256  eirrlem  16282  sadadd2lem2  16530  pythagtriplem12  16908  pythagtriplem15  16911  pythagtriplem17  16913  difsqpwdvds  16969  prmreclem6  17003  4sqlem11  17037  4sqlem12  17038  vdwlem3  17065  vdwlem8  17070  vdwlem9  17071  vdwlem10  17072  bl2in  24608  tcphcphlem1  25445  nmparlem  25449  cphipval2  25451  minveclem2  25636  minveclem4  25642  ovolunlem1  25707  uniioombllem5  25797  sineq0  26740  cosordlem  26746  tanarg  26835  heron  27054  dcubic1  27061  dquartlem1  27067  quart1lem  27071  sinasin  27105  asinsin  27108  cosasin  27120  efiatan2  27133  2efiatan  27134  atantan  27139  atantayl2  27154  leibpi  27158  log2cnv  27160  lgamgulmlem2  27245  lgamgulmlem3  27246  basellem5  27300  basellem6  27301  ppiub  27419  chtublem  27426  chtub  27427  bcctr  27490  pcbcctr  27491  bcmono  27492  bcmax  27493  bcp1ctr  27494  bposlem1  27499  bposlem2  27500  bposlem9  27507  gausslemma2d  27589  lgsquadlem1  27595  chebbnd1lem2  27685  dchrisumlem2  27705  dchrisum0lem1b  27730  mulog2sumlem1  27749  logdivbnd  27771  selberg3lem1  27772  pntrsumbnd2  27782  selbergr  27783  selberg3r  27784  selberg34r  27786  pntpbnd1a  27800  pntpbnd2  27802  pntlemg  27813  pntlemr  27817  pntlemo  27822  ostth2lem1  27833  ostth3  27853  finsumvtxdg2ssteplem4  29956  nrt2irr  30895  nvge0  31096  minvecolem2  31298  minvecolem4  31303  cdj3lem1  32857  binom2subadd  33156  constrrtcc  34189  constraddcl  34216  sqsscirc1  34362  bcprod  36267  unbdqndv2lem1  37155  irrdifflemf  38026  mblfinlem3  38367  ftc1anclem7  38407  areacirclem1  38416  areacirc  38421  isbnd3  38493  lcmineqlem18  42871  aks6d1c7lem1  43005  sumcubes  43132  3cubeslem2  43474  3cubeslem3r  43476  pellfundex  43671  rmxluc  43721  rmyluc  43722  rmxdbl  43724  rmydbl  43725  jm2.24nn  43744  acongeq  43768  jm2.16nn0  43789  jm3.1lem1  43802  jm3.1lem2  43803  sqrtcval  44425  imo72b2lem0  44949  sineq0ALT  45703  sinmulcos  46637  stirlinglem5  46850  fourierdlem79  46957  fouriercnp  46998  hoicvrrex  47328  2leaddle2  48093  modmkpkne  48162  modmknepk  48163  lighneallem4a  48418  gpg5nbgrvtx13starlem2  48895  gpg3kgrtriexlem2  48907  gpg3kgrtriexlem5  48910  nnpw2pmod  49420  itschlc0yqe  49597  sinhpcosh  50575