Theorem 2timesd 12629

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242   · cmul 11244  2c2 12437

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulcom 11303  ax-mulass 11305  ax-distr 11306  ax-1rid 11309  ax-cnre 11312

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445

This theorem is used by:  lt2addmuld  12636  nn0le2x  12700  flhalf  14010  2submod  14115  modaddmodup  14117  m1expeven  14292  expmulnbnd  14420  discr  14425  crre  15324  imval2  15361  abslem2  15551  sqreulem  15571  amgm2  15581  caucvgrlem  15884  iseraltlem2  15894  iseraltlem3  15895  arisum2  16074  fallrisefac  16236  efival  16364  sinadd  16376  cosadd  16377  addsin  16382  subsin  16383  cosmul  16385  addcos  16386  subcos  16387  sin2t  16389  cos2t  16390  eirrlem  16416  sadadd2lem2  16664  pythagtriplem12  17048  pythagtriplem15  17051  pythagtriplem17  17053  difsqpwdvds  17109  prmreclem6  17143  4sqlem11  17177  4sqlem12  17178  vdwlem3  17205  vdwlem8  17210  vdwlem9  17211  vdwlem10  17212  bl2in  24774  tcphcphlem1  25611  nmparlem  25615  cphipval2  25617  minveclem2  25802  minveclem4  25808  ovolunlem1  25873  uniioombllem5  25963  sineq0  26909  cosordlem  26915  tanarg  27004  heron  27223  dcubic1  27230  dquartlem1  27236  quart1lem  27240  sinasin  27274  asinsin  27277  cosasin  27289  efiatan2  27302  2efiatan  27303  atantan  27308  atantayl2  27323  leibpi  27327  log2cnv  27329  lgamgulmlem2  27414  lgamgulmlem3  27415  basellem5  27469  basellem6  27470  ppiub  27588  chtublem  27595  chtub  27596  bcctr  27659  pcbcctr  27660  bcmono  27661  bcmax  27662  bcp1ctr  27663  bposlem1  27668  bposlem2  27669  bposlem9  27676  gausslemma2d  27758  lgsquadlem1  27764  chebbnd1lem2  27854  dchrisumlem2  27874  dchrisum0lem1b  27899  mulog2sumlem1  27918  logdivbnd  27940  selberg3lem1  27941  pntrsumbnd2  27951  selbergr  27952  selberg3r  27953  selberg34r  27955  pntpbnd1a  27969  pntpbnd2  27971  pntlemg  27982  pntlemr  27986  pntlemo  27991  ostth2lem1  28002  ostth3  28022  finsumvtxdg2ssteplem4  30186  nrt2irr  31131  nvge0  31332  minvecolem2  31534  minvecolem4  31539  cdj3lem1  33093  binom2subadd  33429  constrrtcc  34478  constraddcl  34505  sqsscirc1  34651  bcprod  36718  unbdqndv2lem1  37590  irrdifflemf  38514  mblfinlem3  38845  ftc1anclem7  38885  areacirclem1  38894  areacirc  38899  isbnd3  38984  lcmineqlem18  43362  aks6d1c7lem1  43496  sumcubes  43636  3cubeslem2  43961  3cubeslem3r  43963  pellfundex  44159  rmxluc  44209  rmyluc  44210  rmxdbl  44212  rmydbl  44213  jm2.24nn  44232  acongeq  44256  jm2.16nn0  44277  jm3.1lem1  44290  jm3.1lem2  44291  sqrtcval  44902  imo72b2lem0  45426  sineq0ALT  46179  sinmulcos  47148  stirlinglem5  47361  fourierdlem79  47468  fouriercnp  47509  hoicvrrex  47839  2leaddle2  48641  modmkpkne  48710  modmknepk  48711  lighneallem4a  48966  gpg5nbgrvtx13starlem2  49443  gpg3kgrtriexlem2  49455  gpg3kgrtriexlem5  49458  nnpw2pmod  50026  itschlc0yqe  50203  sinhpcosh  51238