Theorem 2timesi 11348

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

Syntax hints:   = wceq 1630   ∈ wcel 2144  (class class class)co 6792  ℂcc 10135   + caddc 10140   · cmul 10142  2c2 11271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-mulcl 10199  ax-mulcom 10201  ax-mulass 10203  ax-distr 10204  ax-1rid 10207  ax-cnre 10210

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-2 11280

This theorem is referenced by:  2t2e4  11378  nn0le2xi  11548  binom2i  13180  rddif  14287  abs3lemi  14356  iseraltlem2  14620  prmreclem6  15831  mod2xi  15979  numexp2x  15989  prmlem2  16033  iihalf2  22951  pcoass  23042  ovolunlem1a  23483  tangtx  24477  sinq34lt0t  24481  eff1o  24515  ang180lem2  24760  dvatan  24882  basellem2  25028  basellem5  25031  chtub  25157  bposlem9  25237  ex-dvds  27649  norm3lem  28340  normpari  28345  polid2i  28348  ballotth  30933  heiborlem6  33940  rmspecsqrtnqOLD  37990  dirkertrigeqlem1  40826  fourierdlem94  40928  fourierdlem102  40936  fourierdlem111  40945  fourierdlem112  40946  fourierdlem113  40947  fourierdlem114  40948  sqwvfoura  40956  sqwvfourb  40957  fouriersw  40959  fmtnorec3  41978  2t6m3t4e0  42644  zlmodzxzequa  42803