Theorem 2timesi 12405

Description: Two times a number. (Contributed by NM, 1-Aug-1999.)

Hypothesis

Ref	Expression
2timesi.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
2timesi	⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Proof of Theorem 2timesi

Step	Hyp	Ref	Expression
1		2timesi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		2times 12403	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Syntax hints:   = wceq 1539   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   + caddc 11159   · cmul 11161  2c2 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-mulcl 11218  ax-mulcom 11220  ax-mulass 11222  ax-distr 11223  ax-1rid 11226  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330

This theorem is referenced by:  2t2e4  12431  binom2i  14252  rddif  15380  abs3lemi  15450  iseraltlem2  15720  prmreclem6  16960  mod2xi  17108  numexp2x  17117  prmlem2  17158  iihalf2  24962  pcoass  25058  ovolunlem1a  25532  tangtx  26548  sinq34lt0t  26552  eff1o  26592  ang180lem2  26854  dvatan  26979  basellem2  27126  basellem5  27129  chtub  27257  bposlem9  27337  ex-dvds  30476  norm3lem  31169  normpari  31174  polid2i  31177  ballotth  34541  heiborlem6  37824  sqsumi  42321  dirkertrigeqlem1  46118  fourierdlem94  46220  fourierdlem102  46228  fourierdlem111  46237  fourierdlem112  46238  fourierdlem113  46239  fourierdlem114  46240  sqwvfoura  46248  sqwvfourb  46249  fouriersw  46251  fmtnorec3  47540  2t6m3t4e0  48269  zlmodzxzequa  48418