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

Theorem 2timesd 9954
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 9843 . 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 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742   2c2 9795
This theorem is referenced by:  fzctr  10854  flhalf  10954  expmulnbnd  11233  discr  11238  crre  11599  imval2  11636  abslem2  11823  sqreulem  11843  amgm2  11853  caucvgrlem  12145  iseraltlem2  12155  iseraltlem3  12156  arisum2  12319  efival  12432  sinadd  12444  cosadd  12445  addsin  12450  subsin  12451  cosmul  12453  addcos  12454  subcos  12455  sin2t  12457  cos2t  12458  eirrlem  12482  sadadd2lem2  12641  pythagtriplem12  12879  pythagtriplem15  12882  pythagtriplem17  12884  prmreclem6  12968  4sqlem11  13002  4sqlem12  13003  vdwlem3  13030  vdwlem8  13035  vdwlem9  13036  vdwlem10  13037  bl2in  17957  tchcphlem1  18665  nmparlem  18669  minveclem2  18790  minveclem4  18796  ovolunlem1  18856  uniioombllem5  18942  sineq0  19889  cosordlem  19893  tanarg  19970  dcubic1  20141  dquartlem1  20147  quart1lem  20151  sinasin  20185  asinsin  20188  cosasin  20200  efiatan2  20213  2efiatan  20214  atantan  20219  atantayl2  20234  leibpi  20238  log2cnv  20240  basellem5  20322  basellem6  20323  ppiub  20443  chtublem  20450  chtub  20451  bcctr  20514  pcbcctr  20515  bcmono  20516  bcmax  20517  bcp1ctr  20518  bposlem1  20523  bposlem2  20524  bposlem9  20531  lgsquadlem1  20593  chebbnd1lem2  20619  dchrisumlem2  20639  dchrisum0lem1b  20664  mulog2sumlem1  20683  logdivbnd  20705  selberg3lem1  20706  pntrsumbnd2  20716  selbergr  20717  selberg3r  20718  selberg34r  20720  pntpbnd1a  20734  pntpbnd2  20736  pntlemg  20747  pntlemr  20751  pntlemo  20756  ostth2lem1  20767  ostth3  20787  nvge0  21240  minvecolem2  21454  minvecolem4  21459  cdj3lem1  23014  areacirclem2  24925  areacirc  24931  mslb1  25607  2wsms  25608  isbnd3  26508  pellfundex  26971  rmxluc  27021  rmyluc  27022  rmxdbl  27024  rmydbl  27025  jm2.24nn  27046  acongeq  27070  jm2.16nn0  27097  jm3.1lem1  27110  jm3.1lem2  27111  stirlinglem5  27827  sinhpcosh  28210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulcom 8801  ax-mulass 8803  ax-distr 8804  ax-1rid 8807  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-2 9804
  Copyright terms: Public domain W3C validator