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	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = - 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2times	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
2	1	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = ( 𝐴 − ( 𝐴 + 𝐴 ) ) )
3		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
4	3 3	addcld	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 𝐴 ) ∈ ℂ )
5	3 4	negsubd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = ( 𝐴 − ( 𝐴 + 𝐴 ) ) )
6	3 3	negdid	⊢ ( 𝐴 ∈ ℂ → - ( 𝐴 + 𝐴 ) = ( - 𝐴 + - 𝐴 ) )
7	6	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = ( 𝐴 + ( - 𝐴 + - 𝐴 ) ) )
8		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
9	3 8 8	addassd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = ( 𝐴 + ( - 𝐴 + - 𝐴 ) ) )
10		negid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )
11	10	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = ( 0 + - 𝐴 ) )
12	8	addid2d	⊢ ( 𝐴 ∈ ℂ → ( 0 + - 𝐴 ) = - 𝐴 )
13	11 12	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 + - 𝐴 ) + - 𝐴 ) = - 𝐴 )
14	7 9 13	3eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + - ( 𝐴 + 𝐴 ) ) = - 𝐴 )
15	2 5 14	3eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( 2 · 𝐴 ) ) = - 𝐴 )