Theorem 2times 12309

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7364  ℂcc 11033  1c1 11036   + caddc 11038   · cmul 11040  2c2 12233

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 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-mulcl 11097  ax-mulcom 11099  ax-mulass 11101  ax-distr 11102  ax-1rid 11105  ax-cnre 11108

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 6452  df-fv 6504  df-ov 7367  df-2 12241

This theorem is referenced by:  times2  12310  2timesi  12311  2txmxeqx  12313  2halves  12392  halfaddsub  12407  avglt2  12413  2timesd  12417  expubnd  14137  absmax  15289  sinmul  16136  sin2t  16141  cos2t  16142  sadadd2lem2  16416  pythagtriplem4  16787  pythagtriplem14  16796  pythagtriplem16  16798  2sqreultlem  27430  2sqreunnltlem  27433  cncph  30911  pellexlem2  43284  acongrep  43434  sub2times  45732  2timesgt  45747