Theorem 2times 11767

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 11694	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7159	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 10804	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	syl5eq 2867	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  (class class class)co 7149  ℂcc 10528  1c1 10531   + caddc 10533   · cmul 10535  2c2 11686

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-mulcl 10592  ax-mulcom 10594  ax-mulass 10596  ax-distr 10597  ax-1rid 10600  ax-cnre 10603

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3493  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5060  df-iota 6307  df-fv 6356  df-ov 7152  df-2 11694

This theorem is referenced by:  times2  11768  2timesi  11769  2txmxeqx  11771  2halves  11859  halfaddsub  11864  avglt2  11870  2timesd  11874  expubnd  13538  absmax  14684  sinmul  15520  sin2t  15525  cos2t  15526  sadadd2lem2  15794  pythagtriplem4  16151  pythagtriplem14  16160  pythagtriplem16  16162  2sqreultlem  26021  2sqreunnltlem  26024  cncph  28594  pellexlem2  39503  acongrep  39653  sub2times  41614  2timesgt  41628