Theorem 2timesi 11496

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

Syntax hints:   = wceq 1658   ∈ wcel 2166  (class class class)co 6905  ℂcc 10250   + caddc 10255   · cmul 10257  2c2 11406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-mulcl 10314  ax-mulcom 10316  ax-mulass 10318  ax-distr 10319  ax-1rid 10322  ax-cnre 10325

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-2 11414

This theorem is referenced by:  2t2e4  11522  nn0le2xi  11674  binom2i  13268  rddif  14457  abs3lemi  14526  iseraltlem2  14790  prmreclem6  15996  mod2xi  16144  numexp2x  16154  prmlem2  16192  iihalf2  23102  pcoass  23193  ovolunlem1a  23662  tangtx  24657  sinq34lt0t  24661  eff1o  24695  ang180lem2  24950  dvatan  25075  basellem2  25221  basellem5  25224  chtub  25350  bposlem9  25430  ex-dvds  27871  norm3lem  28561  normpari  28566  polid2i  28569  ballotth  31145  heiborlem6  34157  sqsumi  38056  dirkertrigeqlem1  41109  fourierdlem94  41211  fourierdlem102  41219  fourierdlem111  41228  fourierdlem112  41229  fourierdlem113  41230  fourierdlem114  41231  sqwvfoura  41239  sqwvfourb  41240  fouriersw  41242  fmtnorec3  42290  2t6m3t4e0  42973  zlmodzxzequa  43132