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

Theorem 2timesd 10787
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 10660 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( 2  x.  A
)  =  ( A  +  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804  (class class class)co 6281   CCcc 9493    + caddc 9498    x. cmul 9500   2c2 10591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-mulcl 9557  ax-mulcom 9559  ax-mulass 9561  ax-distr 9562  ax-1rid 9565  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-2 10600
This theorem is referenced by:  fzctr  11795  flhalf  11941  2submod  12027  modaddmodup  12029  expmulnbnd  12277  discr  12282  crre  12926  imval2  12963  abslem2  13151  sqreulem  13171  amgm2  13181  caucvgrlem  13474  iseraltlem2  13484  iseraltlem3  13485  arisum2  13651  efival  13764  sinadd  13776  cosadd  13777  addsin  13782  subsin  13783  cosmul  13785  addcos  13786  subcos  13787  sin2t  13789  cos2t  13790  eirrlem  13814  sadadd2lem2  13977  pythagtriplem12  14227  pythagtriplem15  14230  pythagtriplem17  14232  prmreclem6  14316  4sqlem11  14350  4sqlem12  14351  vdwlem3  14378  vdwlem8  14383  vdwlem9  14384  vdwlem10  14385  bl2in  20776  tchcphlem1  21551  nmparlem  21555  minveclem2  21714  minveclem4  21720  ovolunlem1  21781  uniioombllem5  21869  sineq0  22786  cosordlem  22790  tanarg  22876  heron  23041  dcubic1  23048  dquartlem1  23054  quart1lem  23058  sinasin  23092  asinsin  23095  cosasin  23107  efiatan2  23120  2efiatan  23121  atantan  23126  atantayl2  23141  leibpi  23145  log2cnv  23147  basellem5  23230  basellem6  23231  ppiub  23351  chtublem  23358  chtub  23359  bcctr  23422  pcbcctr  23423  bcmono  23424  bcmax  23425  bcp1ctr  23426  bposlem1  23431  bposlem2  23432  bposlem9  23439  lgsquadlem1  23501  chebbnd1lem2  23527  dchrisumlem2  23547  dchrisum0lem1b  23572  mulog2sumlem1  23591  logdivbnd  23613  selberg3lem1  23614  pntrsumbnd2  23624  selbergr  23625  selberg3r  23626  selberg34r  23628  pntpbnd1a  23642  pntpbnd2  23644  pntlemg  23655  pntlemr  23659  pntlemo  23664  ostth2lem1  23675  ostth3  23695  nvge0  25449  minvecolem2  25663  minvecolem4  25668  cdj3lem1  27225  sqsscirc1  27763  lgamgulmlem2  28445  lgamgulmlem3  28446  m1expevenALT  28536  fallrisefac  29122  mblfinlem3  30028  ftc1anclem7  30071  areacirclem1  30082  areacirc  30087  isbnd3  30255  pellfundex  30797  rmxluc  30847  rmyluc  30848  rmxdbl  30850  rmydbl  30851  jm2.24nn  30872  acongeq  30896  jm2.16nn0  30921  jm3.1lem1  30934  jm3.1lem2  30935  lt2addmuld  31422  sinmulcos  31572  stirlinglem5  31749  fourierdlem79  31857  fouriercnp  31898  2leaddle2  32158  sinhpcosh  32869  sineq0ALT  33470  imo72b2lem0  37651
  Copyright terms: Public domain W3C validator