Theorem 2times 12280

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028  1c1 11031   + caddc 11033   · cmul 11035  2c2 12204

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 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-mulcom 11094  ax-mulass 11096  ax-distr 11097  ax-1rid 11100  ax-cnre 11103

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363  df-2 12212

This theorem is referenced by:  times2  12281  2timesi  12282  2txmxeqx  12284  2halves  12363  halfaddsub  12378  avglt2  12384  2timesd  12388  expubnd  14105  absmax  15257  sinmul  16101  sin2t  16106  cos2t  16107  sadadd2lem2  16381  pythagtriplem4  16751  pythagtriplem14  16760  pythagtriplem16  16762  2sqreultlem  27418  2sqreunnltlem  27421  cncph  30898  pellexlem2  43139  acongrep  43289  sub2times  45588  2timesgt  45603