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 e. CC -> ( A - ( 2 x. A ) ) = -u A )

Proof

Step	Hyp	Ref	Expression
1		2times	|- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
2	1	oveq2d	|- ( A e. CC -> ( A - ( 2 x. A ) ) = ( A - ( A + A ) ) )
3		id	|- ( A e. CC -> A e. CC )
4	3 3	addcld	|- ( A e. CC -> ( A + A ) e. CC )
5	3 4	negsubd	|- ( A e. CC -> ( A + -u ( A + A ) ) = ( A - ( A + A ) ) )
6	3 3	negdid	|- ( A e. CC -> -u ( A + A ) = ( -u A + -u A ) )
7	6	oveq2d	|- ( A e. CC -> ( A + -u ( A + A ) ) = ( A + ( -u A + -u A ) ) )
8		negcl	|- ( A e. CC -> -u A e. CC )
9	3 8 8	addassd	|- ( A e. CC -> ( ( A + -u A ) + -u A ) = ( A + ( -u A + -u A ) ) )
10		negid	|- ( A e. CC -> ( A + -u A ) = 0 )
11	10	oveq1d	|- ( A e. CC -> ( ( A + -u A ) + -u A ) = ( 0 + -u A ) )
12	8	addid2d	|- ( A e. CC -> ( 0 + -u A ) = -u A )
13	11 12	eqtrd	|- ( A e. CC -> ( ( A + -u A ) + -u A ) = -u A )
14	7 9 13	3eqtr2d	|- ( A e. CC -> ( A + -u ( A + A ) ) = -u A )
15	2 5 14	3eqtr2d	|- ( A e. CC -> ( A - ( 2 x. A ) ) = -u A )