Theorem 2times 12478

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 12405	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7430	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11481	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2807	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203   · cmul 11205  2c2 12397

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405

This theorem is used by:  times2  12479  2timesi  12480  2txmxeqx  12482  2halves  12564  halfaddsub  12579  avglt2  12585  2timesd  12589  expubnd  14321  absmax  15497  sinmul  16340  sin2t  16345  cos2t  16346  sadadd2lem2  16620  pythagtriplem4  16997  pythagtriplem14  17006  pythagtriplem16  17008  2sqreultlem  27774  2sqreunnltlem  27777  cncph  31421  pellexlem2  43837  acongrep  43987  sub2times  46289  2timesgt  46304