Theorem 2times

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)

	Ref	Expression
Assertion	2times	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	oveq1i	⊢ ( 2 · 𝐴 ) = ( ( 1 + 1 ) · 𝐴 )
3		1p1times	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 1 ) · 𝐴 ) = ( 𝐴 + 𝐴 ) )
4	2 3	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )