Theorem mulm1

Description: Product with minus one is negative. (Contributed by NM, 16-Nov-1999)

	Ref	Expression
Assertion	mulm1	|- ( A e. CC -> ( -u 1 x. A ) = -u A )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	|- 1 e. CC
2		mulneg1	|- ( ( 1 e. CC /\ A e. CC ) -> ( -u 1 x. A ) = -u ( 1 x. A ) )
3	1 2	mpan	|- ( A e. CC -> ( -u 1 x. A ) = -u ( 1 x. A ) )
4		mulid2	|- ( A e. CC -> ( 1 x. A ) = A )
5	4	negeqd	|- ( A e. CC -> -u ( 1 x. A ) = -u A )
6	3 5	eqtrd	|- ( A e. CC -> ( -u 1 x. A ) = -u A )