Metamath Proof Explorer

Theorem 2txmxeqx

Description: Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Assertion 2txmxeqx X 2 X X = X


Step Hyp Ref Expression
1 id X X
2 2times X 2 X = X + X
3 1 1 2 mvrladdd X 2 X X = X