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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( X e. CC -> X e. CC )
2		2times	|- ( X e. CC -> ( 2 x. X ) = ( X + X ) )
3	1 1 2	mvrladdd	|- ( X e. CC -> ( ( 2 x. X ) - X ) = X )