Theorem 2times 12277

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 12209	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7368	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11305	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2784	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7358  ℂcc 11025  1c1 11028   + caddc 11030   · cmul 11032  2c2 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-mulcl 11089  ax-mulcom 11091  ax-mulass 11093  ax-distr 11094  ax-1rid 11097  ax-cnre 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-2 12209

This theorem is referenced by:  times2  12278  2timesi  12279  2txmxeqx  12281  2halves  12360  halfaddsub  12375  avglt2  12381  2timesd  12385  expubnd  14102  absmax  15254  sinmul  16098  sin2t  16103  cos2t  16104  sadadd2lem2  16378  pythagtriplem4  16748  pythagtriplem14  16757  pythagtriplem16  16759  2sqreultlem  27398  2sqreunnltlem  27401  cncph  30879  pellexlem2  43261  acongrep  43411  sub2times  45709  2timesgt  45724