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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122   + caddc 11127   · cmul 11129  2c2 12319

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 2147  ax-9 2155  ax-ext 2732  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-mulcl 11186  ax-mulcom 11188  ax-mulass 11190  ax-distr 11191  ax-1rid 11194  ax-cnre 11197

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 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-2 12327

This theorem is used by:  lt2addmuld  12518  nn0le2x  12582  fzctr  13695  flhalf  13891  2submod  13996  modaddmodup  13998  m1expeven  14173  expmulnbnd  14299  discr  14304  crre  15201  imval2  15238  abslem2  15427  sqreulem  15447  amgm2  15457  caucvgrlem  15760  iseraltlem2  15770  iseraltlem3  15771  arisum2  15950  fallrisefac  16112  efival  16240  sinadd  16252  cosadd  16253  addsin  16258  subsin  16259  cosmul  16261  addcos  16262  subcos  16263  sin2t  16265  cos2t  16266  eirrlem  16292  sadadd2lem2  16540  pythagtriplem12  16918  pythagtriplem15  16921  pythagtriplem17  16923  difsqpwdvds  16979  prmreclem6  17013  4sqlem11  17047  4sqlem12  17048  vdwlem3  17075  vdwlem8  17080  vdwlem9  17081  vdwlem10  17082  bl2in  24626  tcphcphlem1  25463  nmparlem  25467  cphipval2  25469  minveclem2  25654  minveclem4  25660  ovolunlem1  25725  uniioombllem5  25815  sineq0  26761  cosordlem  26767  tanarg  26856  heron  27075  dcubic1  27082  dquartlem1  27088  quart1lem  27092  sinasin  27126  asinsin  27129  cosasin  27141  efiatan2  27154  2efiatan  27155  atantan  27160  atantayl2  27175  leibpi  27179  log2cnv  27181  lgamgulmlem2  27266  lgamgulmlem3  27267  basellem5  27321  basellem6  27322  ppiub  27440  chtublem  27447  chtub  27448  bcctr  27511  pcbcctr  27512  bcmono  27513  bcmax  27514  bcp1ctr  27515  bposlem1  27520  bposlem2  27521  bposlem9  27528  gausslemma2d  27610  lgsquadlem1  27616  chebbnd1lem2  27706  dchrisumlem2  27726  dchrisum0lem1b  27751  mulog2sumlem1  27770  logdivbnd  27792  selberg3lem1  27793  pntrsumbnd2  27803  selbergr  27804  selberg3r  27805  selberg34r  27807  pntpbnd1a  27821  pntpbnd2  27823  pntlemg  27834  pntlemr  27838  pntlemo  27843  ostth2lem1  27854  ostth3  27874  finsumvtxdg2ssteplem4  30008  nrt2irr  30953  nvge0  31154  minvecolem2  31356  minvecolem4  31361  cdj3lem1  32915  binom2subadd  33212  constrrtcc  34245  constraddcl  34272  sqsscirc1  34418  bcprod  36317  unbdqndv2lem1  37206  irrdifflemf  38077  mblfinlem3  38408  ftc1anclem7  38448  areacirclem1  38457  areacirc  38462  isbnd3  38534  lcmineqlem18  42912  aks6d1c7lem1  43046  sumcubes  43188  3cubeslem2  43530  3cubeslem3r  43532  pellfundex  43727  rmxluc  43777  rmyluc  43778  rmxdbl  43780  rmydbl  43781  jm2.24nn  43800  acongeq  43824  jm2.16nn0  43845  jm3.1lem1  43858  jm3.1lem2  43859  sqrtcval  44481  imo72b2lem0  45005  sineq0ALT  45759  sinmulcos  46693  stirlinglem5  46906  fourierdlem79  47013  fouriercnp  47054  hoicvrrex  47384  2leaddle2  48186  modmkpkne  48255  modmknepk  48256  lighneallem4a  48511  gpg5nbgrvtx13starlem2  48988  gpg3kgrtriexlem2  49000  gpg3kgrtriexlem5  49003  nnpw2pmod  49513  itschlc0yqe  49690  sinhpcosh  50666