Theorem 2times 12381

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 12308	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7429	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11417	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2777	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138  1c1 11141   + caddc 11143   · cmul 11145  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-mulcl 11202  ax-mulcom 11204  ax-mulass 11206  ax-distr 11207  ax-1rid 11210  ax-cnre 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-2 12308

This theorem is referenced by:  times2  12382  2timesi  12383  2txmxeqx  12385  2halves  12473  halfaddsub  12478  avglt2  12484  2timesd  12488  expubnd  14177  absmax  15312  sinmul  16152  sin2t  16157  cos2t  16158  sadadd2lem2  16428  pythagtriplem4  16791  pythagtriplem14  16800  pythagtriplem16  16802  2sqreultlem  27425  2sqreunnltlem  27428  cncph  30701  pellexlem2  42392  acongrep  42543  sub2times  44792  2timesgt  44808