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

Theorem 2timesi 10434
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 10432 . 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 6086   CCcc 9272    + caddc 9277    x. cmul 9279   2c2 10363
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 2418  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-mulcom 9338  ax-mulass 9340  ax-distr 9341  ax-1rid 9344  ax-cnre 9347
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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-ov 6089  df-2 10372
This theorem is referenced by:  2t2e4  10463  nn0le2xi  10623  binom2i  11967  rddif  12820  abs3lemi  12889  iseraltlem2  13152  prmreclem6  13974  mod2xi  14090  numexp2x  14100  prmlem2  14139  iihalf2  20474  pcoass  20565  ovolunlem1a  20948  tangtx  21936  sinq34lt0t  21940  eff1o  21974  ang180lem2  22175  dvatan  22299  basellem2  22388  basellem5  22391  chtub  22520  bposlem9  22600  ex-dvds  23600  norm3lem  24496  normpari  24501  polid2i  24504  ballotth  26868  heiborlem6  28658  rmspecsqrnq  29190  2t6m3t4e0  30682  zlmodzxzequa  30897
  Copyright terms: Public domain W3C validator