Theorem 2times 11761

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 11688	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq1i 7145	. 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴)
3		1p1times 10800	. 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
4	2, 3	syl5eq 2845	1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529   · cmul 10531  2c2 11680

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulcom 10590  ax-mulass 10592  ax-distr 10593  ax-1rid 10596  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-2 11688

This theorem is referenced by:  times2  11762  2timesi  11763  2txmxeqx  11765  2halves  11853  halfaddsub  11858  avglt2  11864  2timesd  11868  expubnd  13537  absmax  14681  sinmul  15517  sin2t  15522  cos2t  15523  sadadd2lem2  15789  pythagtriplem4  16146  pythagtriplem14  16155  pythagtriplem16  16157  2sqreultlem  26031  2sqreunnltlem  26034  cncph  28602  pellexlem2  39771  acongrep  39921  sub2times  41905  2timesgt  41919