Theorem 2times 12307

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

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  (class class class)co 7359  ℂcc 11032  1c1 11035   + caddc 11037   · cmul 11039  2c2 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-resscn 11091  ax-1cn 11092  ax-icn 11093  ax-addcl 11094  ax-mulcl 11096  ax-mulcom 11098  ax-mulass 11100  ax-distr 11101  ax-1rid 11104  ax-cnre 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362  df-2 12239

This theorem is referenced by:  times2  12308  2timesi  12309  2txmxeqx  12311  2halves  12390  halfaddsub  12405  avglt2  12411  2timesd  12415  expubnd  14135  absmax  15287  sinmul  16134  sin2t  16139  cos2t  16140  sadadd2lem2  16414  pythagtriplem4  16785  pythagtriplem14  16794  pythagtriplem16  16796  2sqreultlem  27431  2sqreunnltlem  27434  cncph  30910  pellexlem2  43288  acongrep  43438  sub2times  45733  2timesgt  45748