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

Theorem 2timesd 11487
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 11357 . 2 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
31, 2syl 17 1 (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  (class class class)co 6814  cc 10146   + caddc 10151   · cmul 10153  2c2 11282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-mulcl 10210  ax-mulcom 10212  ax-mulass 10214  ax-distr 10215  ax-1rid 10218  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-2 11291
This theorem is referenced by:  lt2addmuld  11494  fzctr  12665  flhalf  12845  2submod  12945  modaddmodup  12947  m1expeven  13121  expmulnbnd  13210  discr  13215  crre  14073  imval2  14110  abslem2  14298  sqreulem  14318  amgm2  14328  caucvgrlem  14622  iseraltlem2  14632  iseraltlem3  14633  arisum2  14812  fallrisefac  14975  efival  15101  sinadd  15113  cosadd  15114  addsin  15119  subsin  15120  cosmul  15122  addcos  15123  subcos  15124  sin2t  15126  cos2t  15127  eirrlem  15151  sadadd2lem2  15394  pythagtriplem12  15753  pythagtriplem15  15756  pythagtriplem17  15758  difsqpwdvds  15813  prmreclem6  15847  4sqlem11  15881  4sqlem12  15882  vdwlem3  15909  vdwlem8  15914  vdwlem9  15915  vdwlem10  15916  bl2in  22426  tchcphlem1  23254  nmparlem  23258  cphipval2  23260  minveclem2  23417  minveclem4  23423  ovolunlem1  23485  uniioombllem5  23575  sineq0  24493  cosordlem  24497  tanarg  24585  heron  24785  dcubic1  24792  dquartlem1  24798  quart1lem  24802  sinasin  24836  asinsin  24839  cosasin  24851  efiatan2  24864  2efiatan  24865  atantan  24870  atantayl2  24885  leibpi  24889  log2cnv  24891  lgamgulmlem2  24976  lgamgulmlem3  24977  basellem5  25031  basellem6  25032  ppiub  25149  chtublem  25156  chtub  25157  bcctr  25220  pcbcctr  25221  bcmono  25222  bcmax  25223  bcp1ctr  25224  bposlem1  25229  bposlem2  25230  bposlem9  25237  gausslemma2d  25319  lgsquadlem1  25325  chebbnd1lem2  25379  dchrisumlem2  25399  dchrisum0lem1b  25424  mulog2sumlem1  25443  logdivbnd  25465  selberg3lem1  25466  pntrsumbnd2  25476  selbergr  25477  selberg3r  25478  selberg34r  25480  pntpbnd1a  25494  pntpbnd2  25496  pntlemg  25507  pntlemr  25511  pntlemo  25516  ostth2lem1  25527  ostth3  25547  finsumvtxdg2ssteplem4  26675  nvge0  27858  minvecolem2  28061  minvecolem4  28066  cdj3lem1  29623  sqsscirc1  30284  bcprod  31952  unbdqndv2lem1  32827  mblfinlem3  33779  ftc1anclem7  33822  areacirclem1  33831  areacirc  33836  isbnd3  33914  pellfundex  37970  rmxluc  38021  rmyluc  38022  rmxdbl  38024  rmydbl  38025  jm2.24nn  38046  acongeq  38070  jm2.16nn0  38091  jm3.1lem1  38104  jm3.1lem2  38105  imo72b2lem0  38985  sineq0ALT  39690  sinmulcos  40597  stirlinglem5  40816  fourierdlem79  40923  fouriercnp  40964  hoicvrrex  41294  2leaddle2  41840  lighneallem4a  42053  nnpw2pmod  42905  sinhpcosh  43012
  Copyright terms: Public domain W3C validator