Theorem 2times 12402

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 12329	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7441	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11432	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2789	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158   · cmul 11160  2c2 12321

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulcom 11219  ax-mulass 11221  ax-distr 11222  ax-1rid 11225  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329

This theorem is referenced by:  times2  12403  2timesi  12404  2txmxeqx  12406  2halves  12494  halfaddsub  12499  avglt2  12505  2timesd  12509  expubnd  14217  absmax  15368  sinmul  16208  sin2t  16213  cos2t  16214  sadadd2lem2  16487  pythagtriplem4  16857  pythagtriplem14  16866  pythagtriplem16  16868  2sqreultlem  27491  2sqreunnltlem  27494  cncph  30838  pellexlem2  42841  acongrep  42992  sub2times  45284  2timesgt  45300  gpg3nbgrvtxlem  48023