Metamath Proof Explorer


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 AA2A=A

Proof

Step Hyp Ref Expression
1 2times A2A=A+A
2 1 oveq2d AA2A=AA+A
3 id AA
4 3 3 addcld AA+A
5 3 4 negsubd AA+A+A=AA+A
6 3 3 negdid AA+A=-A+A
7 6 oveq2d AA+A+A=A+A+A
8 negcl AA
9 3 8 8 addassd AA+A+A=A+A+A
10 negid AA+A=0
11 10 oveq1d AA+A+A=0+A
12 8 addlidd A0+A=A
13 11 12 eqtrd AA+A+A=A
14 7 9 13 3eqtr2d AA+A+A=A
15 2 5 14 3eqtr2d AA2A=A