Theorem 2timesi 12520

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237   + caddc 11242   · cmul 11244  2c2 12437

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulcom 11303  ax-mulass 11305  ax-distr 11306  ax-1rid 11309  ax-cnre 11312

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445

This theorem is used by:  2t2e4  12546  binom2i  14397  rddif  15552  abs3lemi  15622  iseraltlem2  15894  prmreclem6  17143  mod2xi  17291  numexp2x  17300  prmlem2  17342  iihalf2  25309  pcoass  25400  ovolunlem1a  25872  tangtx  26891  sinq34lt0t  26895  eff1o  26934  ang180lem2  27195  dvatan  27320  basellem2  27466  basellem5  27469  chtub  27596  bposlem9  27676  ex-dvds  31114  norm3lem  31808  normpari  31813  polid2i  31816  ballotth  35281  heiborlem6  39016  sqsumi  43604  dirkertrigeqlem1  47381  fourierdlem94  47483  fourierdlem102  47491  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fourierdlem114  47503  sqwvfoura  47511  sqwvfourb  47512  fouriersw  47514  goldpolyfactor  48200  fmtnorec3  48906  bru3eq  49756  2t6m3t4e0  49791  zlmodzxzequa  49939