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

Theorem 2timesd 10572
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 10445 . 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 1369    e. wcel 1756  (class class class)co 6096   CCcc 9285    + caddc 9290    x. cmul 9292   2c2 10376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-mulcl 9349  ax-mulcom 9351  ax-mulass 9353  ax-distr 9354  ax-1rid 9357  ax-cnre 9360
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-iota 5386  df-fv 5431  df-ov 6099  df-2 10385
This theorem is referenced by:  fzctr  11534  flhalf  11679  2submod  11765  modaddmodup  11767  expmulnbnd  12001  discr  12006  crre  12608  imval2  12645  abslem2  12832  sqreulem  12852  amgm2  12862  caucvgrlem  13155  iseraltlem2  13165  iseraltlem3  13166  arisum2  13328  efival  13441  sinadd  13453  cosadd  13454  addsin  13459  subsin  13460  cosmul  13462  addcos  13463  subcos  13464  sin2t  13466  cos2t  13467  eirrlem  13491  sadadd2lem2  13651  pythagtriplem12  13898  pythagtriplem15  13901  pythagtriplem17  13903  prmreclem6  13987  4sqlem11  14021  4sqlem12  14022  vdwlem3  14049  vdwlem8  14054  vdwlem9  14055  vdwlem10  14056  bl2in  19980  tchcphlem1  20755  nmparlem  20759  minveclem2  20918  minveclem4  20924  ovolunlem1  20985  uniioombllem5  21072  sineq0  21988  cosordlem  21992  tanarg  22073  heron  22238  dcubic1  22245  dquartlem1  22251  quart1lem  22255  sinasin  22289  asinsin  22292  cosasin  22304  efiatan2  22317  2efiatan  22318  atantan  22323  atantayl2  22338  leibpi  22342  log2cnv  22344  basellem5  22427  basellem6  22428  ppiub  22548  chtublem  22555  chtub  22556  bcctr  22619  pcbcctr  22620  bcmono  22621  bcmax  22622  bcp1ctr  22623  bposlem1  22628  bposlem2  22629  bposlem9  22636  lgsquadlem1  22698  chebbnd1lem2  22724  dchrisumlem2  22744  dchrisum0lem1b  22769  mulog2sumlem1  22788  logdivbnd  22810  selberg3lem1  22811  pntrsumbnd2  22821  selbergr  22822  selberg3r  22823  selberg34r  22825  pntpbnd1a  22839  pntpbnd2  22841  pntlemg  22852  pntlemr  22856  pntlemo  22861  ostth2lem1  22872  ostth3  22892  nvge0  24067  minvecolem2  24281  minvecolem4  24286  cdj3lem1  25843  sqsscirc1  26343  lgamgulmlem2  27021  lgamgulmlem3  27022  m1expevenALT  27112  fallrisefac  27533  mblfinlem3  28435  ftc1anclem7  28478  areacirclem1  28489  areacirc  28494  isbnd3  28688  pellfundex  29232  rmxluc  29282  rmyluc  29283  rmxdbl  29285  rmydbl  29286  jm2.24nn  29307  acongeq  29331  jm2.16nn0  29358  jm3.1lem1  29371  jm3.1lem2  29372  stirlinglem5  29878  2leaddle2  30180  sinhpcosh  31080  sineq0ALT  31678
  Copyright terms: Public domain W3C validator