Theorem 2timesi 12261

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 12259	. 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴)

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   + caddc 11012   · cmul 11014  2c2 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulcom 11073  ax-mulass 11075  ax-distr 11076  ax-1rid 11079  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191

This theorem is referenced by:  2t2e4  12287  binom2i  14119  rddif  15248  abs3lemi  15318  iseraltlem2  15590  prmreclem6  16833  mod2xi  16981  numexp2x  16990  prmlem2  17031  iihalf2  24826  pcoass  24922  ovolunlem1a  25395  tangtx  26412  sinq34lt0t  26416  eff1o  26456  ang180lem2  26718  dvatan  26843  basellem2  26990  basellem5  26993  chtub  27121  bposlem9  27201  ex-dvds  30400  norm3lem  31093  normpari  31098  polid2i  31101  ballotth  34506  heiborlem6  37800  sqsumi  42258  dirkertrigeqlem1  46083  fourierdlem94  46185  fourierdlem102  46193  fourierdlem111  46202  fourierdlem112  46203  fourierdlem113  46204  fourierdlem114  46205  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  fmtnorec3  47536  2t6m3t4e0  48336  zlmodzxzequa  48485