Theorem 2times 12324

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078   · cmul 11080  2c2 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256

This theorem is referenced by:  times2  12325  2timesi  12326  2txmxeqx  12328  2halves  12407  halfaddsub  12422  avglt2  12428  2timesd  12432  expubnd  14150  absmax  15303  sinmul  16147  sin2t  16152  cos2t  16153  sadadd2lem2  16427  pythagtriplem4  16797  pythagtriplem14  16806  pythagtriplem16  16808  2sqreultlem  27365  2sqreunnltlem  27368  cncph  30755  pellexlem2  42825  acongrep  42976  sub2times  45278  2timesgt  45293