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

Theorem 2timesd 10001
Description: Two times a number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
2timesd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
2timesd  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )

Proof of Theorem 2timesd
StepHypRef Expression
1 2timesd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 2times 9890 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2syl 15 1  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633    e. wcel 1701  (class class class)co 5900   CCcc 8780    + caddc 8785    x. cmul 8787   2c2 9840
This theorem is referenced by:  fzctr  10901  flhalf  11001  expmulnbnd  11280  discr  11285  crre  11646  imval2  11683  abslem2  11870  sqreulem  11890  amgm2  11900  caucvgrlem  12192  iseraltlem2  12202  iseraltlem3  12203  arisum2  12366  efival  12479  sinadd  12491  cosadd  12492  addsin  12497  subsin  12498  cosmul  12500  addcos  12501  subcos  12502  sin2t  12504  cos2t  12505  eirrlem  12529  sadadd2lem2  12688  pythagtriplem12  12926  pythagtriplem15  12929  pythagtriplem17  12931  prmreclem6  13015  4sqlem11  13049  4sqlem12  13050  vdwlem3  13077  vdwlem8  13082  vdwlem9  13083  vdwlem10  13084  bl2in  18009  tchcphlem1  18718  nmparlem  18722  minveclem2  18843  minveclem4  18849  ovolunlem1  18909  uniioombllem5  18995  sineq0  19942  cosordlem  19946  tanarg  20023  dcubic1  20194  dquartlem1  20200  quart1lem  20204  sinasin  20238  asinsin  20241  cosasin  20253  efiatan2  20266  2efiatan  20267  atantan  20272  atantayl2  20287  leibpi  20291  log2cnv  20293  basellem5  20375  basellem6  20376  ppiub  20496  chtublem  20503  chtub  20504  bcctr  20567  pcbcctr  20568  bcmono  20569  bcmax  20570  bcp1ctr  20571  bposlem1  20576  bposlem2  20577  bposlem9  20584  lgsquadlem1  20646  chebbnd1lem2  20672  dchrisumlem2  20692  dchrisum0lem1b  20717  mulog2sumlem1  20736  logdivbnd  20758  selberg3lem1  20759  pntrsumbnd2  20769  selbergr  20770  selberg3r  20771  selberg34r  20773  pntpbnd1a  20787  pntpbnd2  20789  pntlemg  20800  pntlemr  20804  pntlemo  20809  ostth2lem1  20820  ostth3  20840  nvge0  21295  minvecolem2  21509  minvecolem4  21514  cdj3lem1  23069  areacirclem2  25342  areacirc  25348  isbnd3  25656  pellfundex  26119  rmxluc  26169  rmyluc  26170  rmxdbl  26172  rmydbl  26173  jm2.24nn  26194  acongeq  26218  jm2.16nn0  26245  jm3.1lem1  26258  jm3.1lem2  26259  stirlinglem5  26975  sinhpcosh  27659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-mulcl 8844  ax-mulcom 8846  ax-mulass 8848  ax-distr 8849  ax-1rid 8852  ax-cnre 8855
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-2 9849
  Copyright terms: Public domain W3C validator