Theorem 2times 12290

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 12222	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7380	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11318	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2784	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7370  ℂcc 11038  1c1 11041   + caddc 11043   · cmul 11045  2c2 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-mulcl 11102  ax-mulcom 11104  ax-mulass 11106  ax-distr 11107  ax-1rid 11110  ax-cnre 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373  df-2 12222

This theorem is referenced by:  times2  12291  2timesi  12292  2txmxeqx  12294  2halves  12373  halfaddsub  12388  avglt2  12394  2timesd  12398  expubnd  14115  absmax  15267  sinmul  16111  sin2t  16116  cos2t  16117  sadadd2lem2  16391  pythagtriplem4  16761  pythagtriplem14  16770  pythagtriplem16  16772  2sqreultlem  27431  2sqreunnltlem  27434  cncph  30913  pellexlem2  43216  acongrep  43366  sub2times  45664  2timesgt  45679