Description: Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | sub2times | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2times | |
|
2 | 1 | oveq2d | |
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 | |
|
11 | 10 | oveq1d | |
12 | 8 | addlidd | |
13 | 11 12 | eqtrd | |
14 | 7 9 13 | 3eqtr2d | |
15 | 2 5 14 | 3eqtr2d | |