Theorem 2times 12433

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7409  ℂcc 11155  1c1 11158   + caddc 11160   · cmul 11162  2c2 12352

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-mulcl 11219  ax-mulcom 11221  ax-mulass 11223  ax-distr 11224  ax-1rid 11227  ax-cnre 11230

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412  df-2 12360

This theorem is used by:  times2  12434  2timesi  12435  2txmxeqx  12437  2halves  12519  halfaddsub  12534  avglt2  12540  2timesd  12544  expubnd  14275  absmax  15450  sinmul  16293  sin2t  16298  cos2t  16299  sadadd2lem2  16573  pythagtriplem4  16944  pythagtriplem14  16953  pythagtriplem16  16955  2sqreultlem  27723  2sqreunnltlem  27726  cncph  31340  pellexlem2  43769  acongrep  43919  sub2times  46204  2timesgt  46219