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

Theorem 2timesi 9845
Description: Two times a number. (Contributed by NM, 1-Aug-1999.)
Hypothesis
Ref Expression
2times.1  |-  A  e.  CC
Assertion
Ref Expression
2timesi  |-  ( 2  x.  A )  =  ( A  +  A
)

Proof of Theorem 2timesi
StepHypRef Expression
1 2times.1 . 2  |-  A  e.  CC
2 2times 9843 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2ax-mp 8 1  |-  ( 2  x.  A )  =  ( A  +  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742   2c2 9795
This theorem is referenced by:  2t2e4  9871  nn0le2xi  10015  binom2i  11212  rddif  11824  abs3lemi  11893  iseraltlem2  12155  prmreclem6  12968  mod2xi  13084  numexp2x  13094  prmlem2  13121  iihalf2  18431  pcoass  18522  ovolunlem1a  18855  tangtx  19873  sinq34lt0t  19877  eff1o  19911  ang180lem2  20108  dvatan  20231  basellem2  20319  basellem5  20322  chtub  20451  bposlem9  20531  ex-dvds  20835  norm3lem  21728  normpari  21733  polid2i  21736  ballotth  23096  3timesi  24590  heiborlem6  25952  rmspecsqrnq  26403
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