Theorem 2timesd 12582

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 12471	. 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 7418  ℂcc 11191   + caddc 11196   · cmul 11198  2c2 12390

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 2733  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-mulcl 11255  ax-mulcom 11257  ax-mulass 11259  ax-distr 11260  ax-1rid 11263  ax-cnre 11266

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  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 6493  df-fv 6545  df-ov 7421  df-2 12398

This theorem is used by:  lt2addmuld  12589  nn0le2x  12653  fzctr  13767  flhalf  13963  2submod  14068  modaddmodup  14070  m1expeven  14245  expmulnbnd  14372  discr  14377  crre  15274  imval2  15311  abslem2  15500  sqreulem  15520  amgm2  15530  caucvgrlem  15833  iseraltlem2  15843  iseraltlem3  15844  arisum2  16023  fallrisefac  16185  efival  16313  sinadd  16325  cosadd  16326  addsin  16331  subsin  16332  cosmul  16334  addcos  16335  subcos  16336  sin2t  16338  cos2t  16339  eirrlem  16365  sadadd2lem2  16613  pythagtriplem12  16997  pythagtriplem15  17000  pythagtriplem17  17002  difsqpwdvds  17058  prmreclem6  17092  4sqlem11  17126  4sqlem12  17127  vdwlem3  17154  vdwlem8  17159  vdwlem9  17160  vdwlem10  17161  bl2in  24712  tcphcphlem1  25549  nmparlem  25553  cphipval2  25555  minveclem2  25740  minveclem4  25746  ovolunlem1  25811  uniioombllem5  25901  sineq0  26845  cosordlem  26851  tanarg  26940  heron  27159  dcubic1  27166  dquartlem1  27172  quart1lem  27176  sinasin  27210  asinsin  27213  cosasin  27225  efiatan2  27238  2efiatan  27239  atantan  27244  atantayl2  27259  leibpi  27263  log2cnv  27265  lgamgulmlem2  27350  lgamgulmlem3  27351  basellem5  27405  basellem6  27406  ppiub  27524  chtublem  27531  chtub  27532  bcctr  27595  pcbcctr  27596  bcmono  27597  bcmax  27598  bcp1ctr  27599  bposlem1  27604  bposlem2  27605  bposlem9  27612  gausslemma2d  27694  lgsquadlem1  27700  chebbnd1lem2  27790  dchrisumlem2  27810  dchrisum0lem1b  27835  mulog2sumlem1  27854  logdivbnd  27876  selberg3lem1  27877  pntrsumbnd2  27887  selbergr  27888  selberg3r  27889  selberg34r  27891  pntpbnd1a  27905  pntpbnd2  27907  pntlemg  27918  pntlemr  27922  pntlemo  27927  ostth2lem1  27938  ostth3  27958  finsumvtxdg2ssteplem4  30122  nrt2irr  31067  nvge0  31268  minvecolem2  31470  minvecolem4  31475  cdj3lem1  33029  binom2subadd  33326  constrrtcc  34360  constraddcl  34387  sqsscirc1  34533  bcprod  36482  unbdqndv2lem1  37355  irrdifflemf  38226  mblfinlem3  38557  ftc1anclem7  38597  areacirclem1  38606  areacirc  38611  isbnd3  38698  lcmineqlem18  43076  aks6d1c7lem1  43210  sumcubes  43350  3cubeslem2  43675  3cubeslem3r  43677  pellfundex  43872  rmxluc  43922  rmyluc  43923  rmxdbl  43925  rmydbl  43926  jm2.24nn  43945  acongeq  43969  jm2.16nn0  43990  jm3.1lem1  44003  jm3.1lem2  44004  sqrtcval  44626  imo72b2lem0  45150  sineq0ALT  45904  sinmulcos  46844  stirlinglem5  47057  fourierdlem79  47164  fouriercnp  47205  hoicvrrex  47535  2leaddle2  48337  modmkpkne  48406  modmknepk  48407  lighneallem4a  48662  gpg5nbgrvtx13starlem2  49139  gpg3kgrtriexlem2  49151  gpg3kgrtriexlem5  49154  nnpw2pmod  49664  itschlc0yqe  49841  sinhpcosh  50802