MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2timesd Structured version   Visualization version   GIF version

Theorem 2timesd 11874
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
StepHypRef Expression
1 2timesd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 2times 11767 . 2 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
31, 2syl 17 1 (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  (class class class)co 7150  cc 10529   + caddc 10534   · cmul 10536  2c2 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-mulcom 10595  ax-mulass 10597  ax-distr 10598  ax-1rid 10601  ax-cnre 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153  df-2 11694
This theorem is referenced by:  lt2addmuld  11881  fzctr  13014  flhalf  13195  2submod  13295  modaddmodup  13297  m1expeven  13471  expmulnbnd  13591  discr  13596  crre  14468  imval2  14505  abslem2  14694  sqreulem  14714  amgm2  14724  caucvgrlem  15024  iseraltlem2  15034  iseraltlem3  15035  arisum2  15211  fallrisefac  15374  efival  15500  sinadd  15512  cosadd  15513  addsin  15518  subsin  15519  cosmul  15521  addcos  15522  subcos  15523  sin2t  15525  cos2t  15526  eirrlem  15552  sadadd2lem2  15794  pythagtriplem12  16158  pythagtriplem15  16161  pythagtriplem17  16163  difsqpwdvds  16218  prmreclem6  16252  4sqlem11  16286  4sqlem12  16287  vdwlem3  16314  vdwlem8  16319  vdwlem9  16320  vdwlem10  16321  bl2in  22944  tcphcphlem1  23772  nmparlem  23776  cphipval2  23778  minveclem2  23963  minveclem4  23969  ovolunlem1  24032  uniioombllem5  24122  sineq0  25043  cosordlem  25047  tanarg  25134  heron  25348  dcubic1  25355  dquartlem1  25361  quart1lem  25365  sinasin  25399  asinsin  25402  cosasin  25414  efiatan2  25427  2efiatan  25428  atantan  25433  atantayl2  25448  leibpi  25453  log2cnv  25455  lgamgulmlem2  25540  lgamgulmlem3  25541  basellem5  25595  basellem6  25596  ppiub  25713  chtublem  25720  chtub  25721  bcctr  25784  pcbcctr  25785  bcmono  25786  bcmax  25787  bcp1ctr  25788  bposlem1  25793  bposlem2  25794  bposlem9  25801  gausslemma2d  25883  lgsquadlem1  25889  chebbnd1lem2  25979  dchrisumlem2  25999  dchrisum0lem1b  26024  mulog2sumlem1  26043  logdivbnd  26065  selberg3lem1  26066  pntrsumbnd2  26076  selbergr  26077  selberg3r  26078  selberg34r  26080  pntpbnd1a  26094  pntpbnd2  26096  pntlemg  26107  pntlemr  26111  pntlemo  26116  ostth2lem1  26127  ostth3  26147  finsumvtxdg2ssteplem4  27263  nvge0  28383  minvecolem2  28585  minvecolem4  28590  cdj3lem1  30144  sqsscirc1  31056  bcprod  32873  unbdqndv2lem1  33751  mblfinlem3  34817  ftc1anclem7  34859  areacirclem1  34868  areacirc  34873  isbnd3  34949  3cubeslem2  39166  3cubeslem3r  39168  pellfundex  39367  rmxluc  39417  rmyluc  39418  rmxdbl  39420  rmydbl  39421  jm2.24nn  39440  acongeq  39464  jm2.16nn0  39485  jm3.1lem1  39498  jm3.1lem2  39499  imo72b2lem0  40400  sineq0ALT  41155  sinmulcos  42030  stirlinglem5  42248  fourierdlem79  42355  fouriercnp  42396  hoicvrrex  42723  2leaddle2  43383  lighneallem4a  43624  nnpw2pmod  44545  itschlc0yqe  44649  sinhpcosh  44741
  Copyright terms: Public domain W3C validator