Theorem sub2times

Description: Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	sub2times	$$⊢A\in ℂ\to A-2A=-A$$

Proof

Step	Hyp	Ref	Expression
1		2times	$$⊢A\in ℂ\to 2A=A+A$$
2	1	oveq2d	$$⊢A\in ℂ\to A-2A=A-\left(A+A\right)$$
3		id	$$⊢A\in ℂ\to A\in ℂ$$
4	3 3	addcld	$$⊢A\in ℂ\to A+A\in ℂ$$
5	3 4	negsubd	$$⊢A\in ℂ\to A+\left(-\left(A+A\right)\right)=A-\left(A+A\right)$$
6	3 3	negdid	$$⊢A\in ℂ\to -\left(A+A\right)=-A+\left(-A\right)$$
7	6	oveq2d	$$⊢A\in ℂ\to A+\left(-\left(A+A\right)\right)=A+\left(-A\right)+\left(-A\right)$$
8		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
9	3 8 8	addassd	$$⊢A\in ℂ\to A+\left(-A\right)+\left(-A\right)=A+\left(-A\right)+\left(-A\right)$$
10		negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$
11	10	oveq1d	$$⊢A\in ℂ\to A+\left(-A\right)+\left(-A\right)=0+\left(-A\right)$$
12	8	addid2d	$$⊢A\in ℂ\to 0+\left(-A\right)=-A$$
13	11 12	eqtrd	$$⊢A\in ℂ\to A+\left(-A\right)+\left(-A\right)=-A$$
14	7 9 13	3eqtr2d	$$⊢A\in ℂ\to A+\left(-\left(A+A\right)\right)=-A$$
15	2 5 14	3eqtr2d	$$⊢A\in ℂ\to A-2A=-A$$