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

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

Proof of Theorem 2timesi
StepHypRef Expression
1 2timesi.1 . 2  |-  A  e.  CC
2 2times 10657 . 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 1381    e. wcel 1802  (class class class)co 6278   CCcc 9490    + caddc 9495    x. cmul 9497   2c2 10588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-mulcl 9554  ax-mulcom 9556  ax-mulass 9558  ax-distr 9559  ax-1rid 9562  ax-cnre 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-br 4435  df-iota 5538  df-fv 5583  df-ov 6281  df-2 10597
This theorem is referenced by:  2t2e4  10688  nn0le2xi  10850  binom2i  12253  rddif  13149  abs3lemi  13218  iseraltlem2  13481  prmreclem6  14313  mod2xi  14429  numexp2x  14439  prmlem2  14479  iihalf2  21303  pcoass  21394  ovolunlem1a  21777  tangtx  22767  sinq34lt0t  22771  eff1o  22805  ang180lem2  23011  dvatan  23135  basellem2  23224  basellem5  23227  chtub  23356  bposlem9  23436  ex-dvds  25038  norm3lem  25935  normpari  25940  polid2i  25943  ballotth  28346  heiborlem6  30284  rmspecsqrtnq  30814  dirkertrigeqlem1  31769  fourierdlem94  31872  fourierdlem102  31880  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  fourierdlem114  31892  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  2t6m3t4e0  32665  zlmodzxzequa  32827
  Copyright terms: Public domain W3C validator