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

Theorem 2timesd 11125
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 10995 . 2 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
31, 2syl 17 1 (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  (class class class)co 6527  cc 9791   + caddc 9796   · cmul 9798  2c2 10920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-mulcl 9855  ax-mulcom 9857  ax-mulass 9859  ax-distr 9860  ax-1rid 9863  ax-cnre 9866
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10929
This theorem is referenced by:  lt2addmuld  11132  fzctr  12278  flhalf  12451  2submod  12551  modaddmodup  12553  m1expeven  12727  expmulnbnd  12816  discr  12821  crre  13651  imval2  13688  abslem2  13876  sqreulem  13896  amgm2  13906  caucvgrlem  14200  iseraltlem2  14210  iseraltlem3  14211  arisum2  14381  fallrisefac  14544  efival  14670  sinadd  14682  cosadd  14683  addsin  14688  subsin  14689  cosmul  14691  addcos  14692  subcos  14693  sin2t  14695  cos2t  14696  eirrlem  14720  sadadd2lem2  14959  pythagtriplem12  15318  pythagtriplem15  15321  pythagtriplem17  15323  difsqpwdvds  15378  prmreclem6  15412  4sqlem11  15446  4sqlem12  15447  vdwlem3  15474  vdwlem8  15479  vdwlem9  15480  vdwlem10  15481  bl2in  21963  tchcphlem1  22787  nmparlem  22791  cphipval2  22793  minveclem2  22950  minveclem4  22956  ovolunlem1  23017  uniioombllem5  23106  sineq0  24022  cosordlem  24026  tanarg  24114  heron  24310  dcubic1  24317  dquartlem1  24323  quart1lem  24327  sinasin  24361  asinsin  24364  cosasin  24376  efiatan2  24389  2efiatan  24390  atantan  24395  atantayl2  24410  leibpi  24414  log2cnv  24416  lgamgulmlem2  24501  lgamgulmlem3  24502  basellem5  24556  basellem6  24557  ppiub  24674  chtublem  24681  chtub  24682  bcctr  24745  pcbcctr  24746  bcmono  24747  bcmax  24748  bcp1ctr  24749  bposlem1  24754  bposlem2  24755  bposlem9  24762  gausslemma2d  24844  lgsquadlem1  24850  chebbnd1lem2  24904  dchrisumlem2  24924  dchrisum0lem1b  24949  mulog2sumlem1  24968  logdivbnd  24990  selberg3lem1  24991  pntrsumbnd2  25001  selbergr  25002  selberg3r  25003  selberg34r  25005  pntpbnd1a  25019  pntpbnd2  25021  pntlemg  25032  pntlemr  25036  pntlemo  25041  ostth2lem1  25052  ostth3  25072  nvge0  26706  minvecolem2  26909  minvecolem4  26914  cdj3lem1  28471  sqsscirc1  29076  bcprod  30671  unbdqndv2lem1  31464  mblfinlem3  32412  ftc1anclem7  32455  areacirclem1  32464  areacirc  32469  isbnd3  32547  pellfundex  36262  rmxluc  36313  rmyluc  36314  rmxdbl  36316  rmydbl  36317  jm2.24nn  36338  acongeq  36362  jm2.16nn0  36383  jm3.1lem1  36396  jm3.1lem2  36397  imo72b2lem0  37281  sineq0ALT  37989  sinmulcos  38542  stirlinglem5  38765  fourierdlem79  38872  fouriercnp  38913  hoicvrrex  39240  lighneallem4a  39858  2leaddle2  40161  nnpw2pmod  42167  sinhpcosh  42233
  Copyright terms: Public domain W3C validator