Metamath Proof Explorer

Theorem mulm1i

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

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

Proof

Step Hyp Ref Expression
1 mulm1.1 
 |-  A e. CC
2 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
3 1 2 ax-mp 
 |-  ( -u 1 x. A ) = -u A