Theorem 2timesd 12596

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7424  ℂcc 11205   + caddc 11210   · cmul 11212  2c2 12404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-mulcl 11269  ax-mulcom 11271  ax-mulass 11273  ax-distr 11274  ax-1rid 11277  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412

This theorem is used by:  lt2addmuld  12603  nn0le2x  12667  flhalf  13977  2submod  14082  modaddmodup  14084  m1expeven  14259  expmulnbnd  14386  discr  14391  crre  15290  imval2  15327  abslem2  15516  sqreulem  15536  amgm2  15546  caucvgrlem  15849  iseraltlem2  15859  iseraltlem3  15860  arisum2  16039  fallrisefac  16201  efival  16329  sinadd  16341  cosadd  16342  addsin  16347  subsin  16348  cosmul  16350  addcos  16351  subcos  16352  sin2t  16354  cos2t  16355  eirrlem  16381  sadadd2lem2  16629  pythagtriplem12  17013  pythagtriplem15  17016  pythagtriplem17  17018  difsqpwdvds  17074  prmreclem6  17108  4sqlem11  17142  4sqlem12  17143  vdwlem3  17170  vdwlem8  17175  vdwlem9  17176  vdwlem10  17177  bl2in  24728  tcphcphlem1  25565  nmparlem  25569  cphipval2  25571  minveclem2  25756  minveclem4  25762  ovolunlem1  25827  uniioombllem5  25917  sineq0  26861  cosordlem  26867  tanarg  26956  heron  27175  dcubic1  27182  dquartlem1  27188  quart1lem  27192  sinasin  27226  asinsin  27229  cosasin  27241  efiatan2  27254  2efiatan  27255  atantan  27260  atantayl2  27275  leibpi  27279  log2cnv  27281  lgamgulmlem2  27366  lgamgulmlem3  27367  basellem5  27421  basellem6  27422  ppiub  27540  chtublem  27547  chtub  27548  bcctr  27611  pcbcctr  27612  bcmono  27613  bcmax  27614  bcp1ctr  27615  bposlem1  27620  bposlem2  27621  bposlem9  27628  gausslemma2d  27710  lgsquadlem1  27716  chebbnd1lem2  27806  dchrisumlem2  27826  dchrisum0lem1b  27851  mulog2sumlem1  27870  logdivbnd  27892  selberg3lem1  27893  pntrsumbnd2  27903  selbergr  27904  selberg3r  27905  selberg34r  27907  pntpbnd1a  27921  pntpbnd2  27923  pntlemg  27934  pntlemr  27938  pntlemo  27943  ostth2lem1  27954  ostth3  27974  finsumvtxdg2ssteplem4  30138  nrt2irr  31083  nvge0  31284  minvecolem2  31486  minvecolem4  31491  cdj3lem1  33045  binom2subadd  33383  constrrtcc  34417  constraddcl  34444  sqsscirc1  34590  bcprod  36599  unbdqndv2lem1  37471  irrdifflemf  38355  mblfinlem3  38686  ftc1anclem7  38726  areacirclem1  38735  areacirc  38740  isbnd3  38827  lcmineqlem18  43205  aks6d1c7lem1  43339  sumcubes  43479  3cubeslem2  43804  3cubeslem3r  43806  pellfundex  44002  rmxluc  44052  rmyluc  44053  rmxdbl  44055  rmydbl  44056  jm2.24nn  44075  acongeq  44099  jm2.16nn0  44120  jm3.1lem1  44133  jm3.1lem2  44134  sqrtcval  44750  imo72b2lem0  45274  sineq0ALT  46027  sinmulcos  46983  stirlinglem5  47196  fourierdlem79  47303  fouriercnp  47344  hoicvrrex  47674  2leaddle2  48476  modmkpkne  48545  modmknepk  48546  lighneallem4a  48801  gpg5nbgrvtx13starlem2  49278  gpg3kgrtriexlem2  49290  gpg3kgrtriexlem5  49293  nnpw2pmod  49803  itschlc0yqe  49980  sinhpcosh  51016