Theorem 2times 12211

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 12138	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7348	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11248	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2788	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  (class class class)co 7338  ℂcc 10971  1c1 10974   + caddc 10976   · cmul 10978  2c2 12130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-mulcl 11035  ax-mulcom 11037  ax-mulass 11039  ax-distr 11040  ax-1rid 11043  ax-cnre 11046

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-iota 6432  df-fv 6488  df-ov 7341  df-2 12138

This theorem is referenced by:  times2  12212  2timesi  12213  2txmxeqx  12215  2halves  12303  halfaddsub  12308  avglt2  12314  2timesd  12318  expubnd  13997  absmax  15141  sinmul  15981  sin2t  15986  cos2t  15987  sadadd2lem2  16257  pythagtriplem4  16618  pythagtriplem14  16627  pythagtriplem16  16629  2sqreultlem  26702  2sqreunnltlem  26705  cncph  29470  pellexlem2  40965  acongrep  41116  sub2times  43200  2timesgt  43214