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

Theorem 2timesi 10463
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 10461 . 2  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
31, 2ax-mp 5 1  |-  ( 2  x.  A )  =  ( A  +  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756  (class class class)co 6112   CCcc 9301    + caddc 9306    x. cmul 9308   2c2 10392
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 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-mulcl 9365  ax-mulcom 9367  ax-mulass 9369  ax-distr 9370  ax-1rid 9373  ax-cnre 9376
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 2577  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-2 10401
This theorem is referenced by:  2t2e4  10492  nn0le2xi  10652  binom2i  11996  rddif  12849  abs3lemi  12918  iseraltlem2  13181  prmreclem6  14003  mod2xi  14119  numexp2x  14129  prmlem2  14168  iihalf2  20527  pcoass  20618  ovolunlem1a  21001  tangtx  21989  sinq34lt0t  21993  eff1o  22027  ang180lem2  22228  dvatan  22352  basellem2  22441  basellem5  22444  chtub  22573  bposlem9  22653  ex-dvds  23677  norm3lem  24573  normpari  24578  polid2i  24581  ballotth  26942  heiborlem6  28741  rmspecsqrnq  29273  2t6m3t4e0  30769  zlmodzxzequa  31035
  Copyright terms: Public domain W3C validator