Theorem 2timesd 12464

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071   + caddc 11076   · cmul 11078  2c2 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-mulcom 11137  ax-mulass 11139  ax-distr 11140  ax-1rid 11143  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280

This theorem is referenced by:  lt2addmuld  12471  nn0le2x  12535  fzctr  13645  flhalf  13840  2submod  13945  modaddmodup  13947  m1expeven  14122  expmulnbnd  14248  discr  14253  crre  15141  imval2  15178  abslem2  15367  sqreulem  15387  amgm2  15397  caucvgrlem  15700  iseraltlem2  15710  iseraltlem3  15711  arisum2  15891  fallrisefac  16055  efival  16184  sinadd  16196  cosadd  16197  addsin  16202  subsin  16203  cosmul  16205  addcos  16206  subcos  16207  sin2t  16209  cos2t  16210  eirrlem  16236  sadadd2lem2  16484  pythagtriplem12  16862  pythagtriplem15  16865  pythagtriplem17  16867  difsqpwdvds  16923  prmreclem6  16957  4sqlem11  16991  4sqlem12  16992  vdwlem3  17019  vdwlem8  17024  vdwlem9  17025  vdwlem10  17026  bl2in  24457  tcphcphlem1  25294  nmparlem  25298  cphipval2  25300  minveclem2  25485  minveclem4  25491  ovolunlem1  25556  uniioombllem5  25646  sineq0  26586  cosordlem  26592  tanarg  26681  heron  26900  dcubic1  26907  dquartlem1  26913  quart1lem  26917  sinasin  26951  asinsin  26954  cosasin  26966  efiatan2  26979  2efiatan  26980  atantan  26985  atantayl2  27000  leibpi  27004  log2cnv  27006  lgamgulmlem2  27091  lgamgulmlem3  27092  basellem5  27146  basellem6  27147  ppiub  27265  chtublem  27272  chtub  27273  bcctr  27336  pcbcctr  27337  bcmono  27338  bcmax  27339  bcp1ctr  27340  bposlem1  27345  bposlem2  27346  bposlem9  27353  gausslemma2d  27435  lgsquadlem1  27441  chebbnd1lem2  27531  dchrisumlem2  27551  dchrisum0lem1b  27576  mulog2sumlem1  27595  logdivbnd  27617  selberg3lem1  27618  pntrsumbnd2  27628  selbergr  27629  selberg3r  27630  selberg34r  27632  pntpbnd1a  27646  pntpbnd2  27648  pntlemg  27659  pntlemr  27663  pntlemo  27668  ostth2lem1  27679  ostth3  27699  finsumvtxdg2ssteplem4  29746  nrt2irr  30672  nvge0  30873  minvecolem2  31075  minvecolem4  31080  cdj3lem1  32634  binom2subadd  32940  constrrtcc  34029  constraddcl  34056  sqsscirc1  34202  bcprod  36085  unbdqndv2lem1  36944  irrdifflemf  37814  mblfinlem3  38155  ftc1anclem7  38195  areacirclem1  38204  areacirc  38209  isbnd3  38280  lcmineqlem18  42660  aks6d1c7lem1  42794  sumcubes  42919  3cubeslem2  43263  3cubeslem3r  43265  pellfundex  43460  rmxluc  43510  rmyluc  43511  rmxdbl  43513  rmydbl  43514  jm2.24nn  43533  acongeq  43557  jm2.16nn0  43578  jm3.1lem1  43591  jm3.1lem2  43592  sqrtcval  44214  imo72b2lem0  44738  sineq0ALT  45509  sinmulcos  46436  stirlinglem5  46649  fourierdlem79  46756  fouriercnp  46797  hoicvrrex  47127  2leaddle2  47889  modmkpkne  47958  modmknepk  47959  lighneallem4a  48214  gpg5nbgrvtx13starlem2  48691  gpg3kgrtriexlem2  48703  gpg3kgrtriexlem5  48706  nnpw2pmod  49202  itschlc0yqe  49379  sinhpcosh  50358