Theorem 2times 12355

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 12282	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7408	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 11356	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	eqtrid 2811	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144  (class class class)co 7398  ℂcc 11073  1c1 11076   + caddc 11078   · cmul 11080  2c2 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulcom 11139  ax-mulass 11141  ax-distr 11142  ax-1rid 11145  ax-cnre 11148

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401  df-2 12282

This theorem is referenced by:  times2  12356  2timesi  12357  2txmxeqx  12359  2halves  12441  halfaddsub  12456  avglt2  12462  2timesd  12466  expubnd  14193  absmax  15359  sinmul  16206  sin2t  16211  cos2t  16212  sadadd2lem2  16486  pythagtriplem4  16857  pythagtriplem14  16866  pythagtriplem16  16868  2sqreultlem  27513  2sqreunnltlem  27516  cncph  31024  pellexlem2  43412  acongrep  43562  sub2times  45857  2timesgt  45872