Theorem 2timesi 12111

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874   · cmul 10876  2c2 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-mulcom 10935  ax-mulass 10937  ax-distr 10938  ax-1rid 10941  ax-cnre 10944

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-2 12036

This theorem is referenced by:  2t2e4  12137  nn0le2xi  12287  binom2i  13928  rddif  15052  abs3lemi  15122  iseraltlem2  15394  prmreclem6  16622  mod2xi  16770  numexp2x  16780  prmlem2  16821  iihalf2  24096  pcoass  24187  ovolunlem1a  24660  tangtx  25662  sinq34lt0t  25666  eff1o  25705  ang180lem2  25960  dvatan  26085  basellem2  26231  basellem5  26234  chtub  26360  bposlem9  26440  ex-dvds  28820  norm3lem  29511  normpari  29516  polid2i  29519  ballotth  32504  heiborlem6  35974  sqsumi  40309  dirkertrigeqlem1  43639  fourierdlem94  43741  fourierdlem102  43749  fourierdlem111  43758  fourierdlem112  43759  fourierdlem113  43760  fourierdlem114  43761  sqwvfoura  43769  sqwvfourb  43770  fouriersw  43772  fmtnorec3  45000  2t6m3t4e0  45684  zlmodzxzequa  45837