Theorem 2timesi 11763

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529   · cmul 10531  2c2 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688

This theorem is referenced by:  2t2e4  11789  nn0le2xi  11939  binom2i  13570  rddif  14692  abs3lemi  14762  iseraltlem2  15031  prmreclem6  16247  mod2xi  16395  numexp2x  16405  prmlem2  16445  iihalf2  23538  pcoass  23629  ovolunlem1a  24100  tangtx  25098  sinq34lt0t  25102  eff1o  25141  ang180lem2  25396  dvatan  25521  basellem2  25667  basellem5  25670  chtub  25796  bposlem9  25876  ex-dvds  28241  norm3lem  28932  normpari  28937  polid2i  28940  ballotth  31905  heiborlem6  35254  sqsumi  39475  dirkertrigeqlem1  42740  fourierdlem94  42842  fourierdlem102  42850  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fourierdlem114  42862  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  fmtnorec3  44065  2t6m3t4e0  44750  zlmodzxzequa  44905