Theorem 2timesi 12405

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125   + caddc 11130   · cmul 11132  2c2 12322

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 2732  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

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 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7417  df-2 12330

This theorem is used by:  2t2e4  12431  binom2i  14279  rddif  15431  abs3lemi  15501  iseraltlem2  15773  prmreclem6  17016  mod2xi  17164  numexp2x  17173  prmlem2  17215  iihalf2  25164  pcoass  25255  ovolunlem1a  25727  tangtx  26746  sinq34lt0t  26750  eff1o  26789  ang180lem2  27050  dvatan  27175  basellem2  27321  basellem5  27324  chtub  27451  bposlem9  27531  ex-dvds  30939  norm3lem  31633  normpari  31638  polid2i  31641  ballotth  35052  heiborlem6  38569  sqsumi  43159  dirkertrigeqlem1  46929  fourierdlem94  47031  fourierdlem102  47039  fourierdlem111  47048  fourierdlem112  47049  fourierdlem113  47050  fourierdlem114  47051  sqwvfoura  47059  sqwvfourb  47060  fouriersw  47062  goldpolyfactor  47748  fmtnorec3  48454  2t6m3t4e0  49281  zlmodzxzequa  49429