Theorem 2timesi 12480

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198   + caddc 11203   · cmul 11205  2c2 12397

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405

This theorem is used by:  2t2e4  12506  binom2i  14356  rddif  15508  abs3lemi  15578  iseraltlem2  15850  prmreclem6  17099  mod2xi  17247  numexp2x  17256  prmlem2  17298  iihalf2  25254  pcoass  25345  ovolunlem1a  25817  tangtx  26834  sinq34lt0t  26838  eff1o  26877  ang180lem2  27138  dvatan  27263  basellem2  27409  basellem5  27412  chtub  27539  bposlem9  27619  ex-dvds  31057  norm3lem  31751  normpari  31756  polid2i  31759  ballotth  35170  heiborlem6  38750  sqsumi  43338  dirkertrigeqlem1  47107  fourierdlem94  47209  fourierdlem102  47217  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  fourierdlem114  47229  sqwvfoura  47237  sqwvfourb  47238  fouriersw  47240  goldpolyfactor  47926  fmtnorec3  48632  2t6m3t4e0  49459  zlmodzxzequa  49607