Theorem 2timesi 12490

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208   + caddc 11213   · cmul 11215  2c2 12407

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-mulcl 11272  ax-mulcom 11274  ax-mulass 11276  ax-distr 11277  ax-1rid 11280  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415

This theorem is used by:  2t2e4  12516  binom2i  14366  rddif  15520  abs3lemi  15590  iseraltlem2  15862  prmreclem6  17111  mod2xi  17259  numexp2x  17268  prmlem2  17310  iihalf2  25266  pcoass  25357  ovolunlem1a  25829  tangtx  26846  sinq34lt0t  26850  eff1o  26889  ang180lem2  27150  dvatan  27275  basellem2  27421  basellem5  27424  chtub  27551  bposlem9  27631  ex-dvds  31069  norm3lem  31763  normpari  31768  polid2i  31771  ballotth  35223  heiborlem6  38890  sqsumi  43478  dirkertrigeqlem1  47247  fourierdlem94  47349  fourierdlem102  47357  fourierdlem111  47366  fourierdlem112  47367  fourierdlem113  47368  fourierdlem114  47369  sqwvfoura  47377  sqwvfourb  47378  fouriersw  47380  goldpolyfactor  48066  fmtnorec3  48772  2t6m3t4e0  49599  zlmodzxzequa  49747