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

Theorem 2timesd 10563
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 10436 . 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 1364    e. wcel 1761  (class class class)co 6090   CCcc 9276    + caddc 9281    x. cmul 9283   2c2 10367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-mulcl 9340  ax-mulcom 9342  ax-mulass 9344  ax-distr 9345  ax-1rid 9348  ax-cnre 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093  df-2 10376
This theorem is referenced by:  fzctr  11525  flhalf  11670  2submod  11756  modaddmodup  11758  expmulnbnd  11992  discr  11997  crre  12599  imval2  12636  abslem2  12823  sqreulem  12843  amgm2  12853  caucvgrlem  13146  iseraltlem2  13156  iseraltlem3  13157  arisum2  13319  efival  13432  sinadd  13444  cosadd  13445  addsin  13450  subsin  13451  cosmul  13453  addcos  13454  subcos  13455  sin2t  13457  cos2t  13458  eirrlem  13482  sadadd2lem2  13642  pythagtriplem12  13889  pythagtriplem15  13892  pythagtriplem17  13894  prmreclem6  13978  4sqlem11  14012  4sqlem12  14013  vdwlem3  14040  vdwlem8  14045  vdwlem9  14046  vdwlem10  14047  bl2in  19934  tchcphlem1  20709  nmparlem  20713  minveclem2  20872  minveclem4  20878  ovolunlem1  20939  uniioombllem5  21026  sineq0  21942  cosordlem  21946  tanarg  22027  heron  22192  dcubic1  22199  dquartlem1  22205  quart1lem  22209  sinasin  22243  asinsin  22246  cosasin  22258  efiatan2  22271  2efiatan  22272  atantan  22277  atantayl2  22292  leibpi  22296  log2cnv  22298  basellem5  22381  basellem6  22382  ppiub  22502  chtublem  22509  chtub  22510  bcctr  22573  pcbcctr  22574  bcmono  22575  bcmax  22576  bcp1ctr  22577  bposlem1  22582  bposlem2  22583  bposlem9  22590  lgsquadlem1  22652  chebbnd1lem2  22678  dchrisumlem2  22698  dchrisum0lem1b  22723  mulog2sumlem1  22742  logdivbnd  22764  selberg3lem1  22765  pntrsumbnd2  22775  selbergr  22776  selberg3r  22777  selberg34r  22779  pntpbnd1a  22793  pntpbnd2  22795  pntlemg  22806  pntlemr  22810  pntlemo  22815  ostth2lem1  22826  ostth3  22846  nvge0  23997  minvecolem2  24211  minvecolem4  24216  cdj3lem1  25773  sqsscirc1  26274  lgamgulmlem2  26946  lgamgulmlem3  26947  m1expevenALT  27037  fallrisefac  27457  mblfinlem3  28355  ftc1anclem7  28398  areacirclem1  28409  areacirc  28414  isbnd3  28608  pellfundex  29152  rmxluc  29202  rmyluc  29203  rmxdbl  29205  rmydbl  29206  jm2.24nn  29227  acongeq  29251  jm2.16nn0  29278  jm3.1lem1  29291  jm3.1lem2  29292  stirlinglem5  29798  2leaddle2  30100  sinhpcosh  30916  sineq0ALT  31507
  Copyright terms: Public domain W3C validator