Theorem 2timesd 12507

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 17	1 ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   + caddc 11156   · cmul 11158  2c2 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-mulcom 11217  ax-mulass 11219  ax-distr 11220  ax-1rid 11223  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327

This theorem is referenced by:  lt2addmuld  12514  nn0le2x  12578  fzctr  13677  flhalf  13867  2submod  13970  modaddmodup  13972  m1expeven  14147  expmulnbnd  14271  discr  14276  crre  15150  imval2  15187  abslem2  15375  sqreulem  15395  amgm2  15405  caucvgrlem  15706  iseraltlem2  15716  iseraltlem3  15717  arisum2  15894  fallrisefac  16058  efival  16185  sinadd  16197  cosadd  16198  addsin  16203  subsin  16204  cosmul  16206  addcos  16207  subcos  16208  sin2t  16210  cos2t  16211  eirrlem  16237  sadadd2lem2  16484  pythagtriplem12  16860  pythagtriplem15  16863  pythagtriplem17  16865  difsqpwdvds  16921  prmreclem6  16955  4sqlem11  16989  4sqlem12  16990  vdwlem3  17017  vdwlem8  17022  vdwlem9  17023  vdwlem10  17024  bl2in  24426  tcphcphlem1  25283  nmparlem  25287  cphipval2  25289  minveclem2  25474  minveclem4  25480  ovolunlem1  25546  uniioombllem5  25636  sineq0  26581  cosordlem  26587  tanarg  26676  heron  26896  dcubic1  26903  dquartlem1  26909  quart1lem  26913  sinasin  26947  asinsin  26950  cosasin  26962  efiatan2  26975  2efiatan  26976  atantan  26981  atantayl2  26996  leibpi  27000  log2cnv  27002  lgamgulmlem2  27088  lgamgulmlem3  27089  basellem5  27143  basellem6  27144  ppiub  27263  chtublem  27270  chtub  27271  bcctr  27334  pcbcctr  27335  bcmono  27336  bcmax  27337  bcp1ctr  27338  bposlem1  27343  bposlem2  27344  bposlem9  27351  gausslemma2d  27433  lgsquadlem1  27439  chebbnd1lem2  27529  dchrisumlem2  27549  dchrisum0lem1b  27574  mulog2sumlem1  27593  logdivbnd  27615  selberg3lem1  27616  pntrsumbnd2  27626  selbergr  27627  selberg3r  27628  selberg34r  27630  pntpbnd1a  27644  pntpbnd2  27646  pntlemg  27657  pntlemr  27661  pntlemo  27666  ostth2lem1  27677  ostth3  27697  finsumvtxdg2ssteplem4  29581  nrt2irr  30502  nvge0  30702  minvecolem2  30904  minvecolem4  30909  cdj3lem1  32463  constrrtcc  33741  sqsscirc1  33869  bcprod  35718  unbdqndv2lem1  36492  irrdifflemf  37308  mblfinlem3  37646  ftc1anclem7  37686  areacirclem1  37695  areacirc  37700  isbnd3  37771  lcmineqlem18  42028  aks6d1c7lem1  42162  2xp3dxp2ge1d  42223  sumcubes  42326  3cubeslem2  42673  3cubeslem3r  42675  pellfundex  42874  rmxluc  42925  rmyluc  42926  rmxdbl  42928  rmydbl  42929  jm2.24nn  42948  acongeq  42972  jm2.16nn0  42993  jm3.1lem1  43006  jm3.1lem2  43007  sqrtcval  43631  imo72b2lem0  44155  sineq0ALT  44935  sinmulcos  45821  stirlinglem5  46034  fourierdlem79  46141  fouriercnp  46182  hoicvrrex  46512  2leaddle2  47248  lighneallem4a  47533  gpg5nbgrvtx13starlem2  47963  nnpw2pmod  48433  itschlc0yqe  48610  sinhpcosh  48971