Theorem 2times 11347

Description: Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)

Assertion

Ref	Expression
2times	⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Proof of Theorem 2times

Step	Hyp	Ref	Expression
1		df-2 11281	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 6803	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 10409	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	syl5eq 2817	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145  (class class class)co 6793  ℂcc 10136  1c1 10139   + caddc 10141   · cmul 10143  2c2 11272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-mulcl 10200  ax-mulcom 10202  ax-mulass 10204  ax-distr 10205  ax-1rid 10208  ax-cnre 10211

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-2 11281

This theorem is referenced by:  times2  11348  2timesi  11349  2txmxeqx  11351  2halves  11462  halfaddsub  11467  avglt2  11473  2timesd  11477  expubnd  13128  subsq2  13180  absmax  14277  sinmul  15108  sin2t  15113  cos2t  15114  sadadd2lem2  15380  pythagtriplem4  15731  pythagtriplem14  15740  pythagtriplem16  15742  cncph  28014  pellexlem2  37920  acongrep  38073  sub2times  40003  2timesgt  40018