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	$$⊢A\in ℂ\to 2A=A+A$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	oveq1i	$$⊢2A=\left(1+1\right)A$$
3		1p1times	$$⊢A\in ℂ\to \left(1+1\right)A=A+A$$
4	2 3	eqtrid	$$⊢A\in ℂ\to 2A=A+A$$