Theorem 2times 12375

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 12302	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7420	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11380	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2808	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  1c1 11100   + caddc 11102   · cmul 11104  2c2 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-mulcom 11163  ax-mulass 11165  ax-distr 11166  ax-1rid 11169  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12302

This theorem is referenced by:  times2  12376  2timesi  12377  2txmxeqx  12379  2halves  12461  halfaddsub  12476  avglt2  12482  2timesd  12486  expubnd  14213  absmax  15380  sinmul  16227  sin2t  16232  cos2t  16233  sadadd2lem2  16507  pythagtriplem4  16878  pythagtriplem14  16887  pythagtriplem16  16889  2sqreultlem  27587  2sqreunnltlem  27590  cncph  31137  pellexlem2  43505  acongrep  43655  sub2times  45940  2timesgt  45955