Theorem mulm1i

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

	Ref	Expression
Hypothesis	mulm1.1	⊢ 𝐴 ∈ ℂ
Assertion	mulm1i	⊢ ( - 1 · 𝐴 ) = - 𝐴

Proof

Step	Hyp	Ref	Expression
1		mulm1.1	⊢ 𝐴 ∈ ℂ
2		mulm1	⊢ ( 𝐴 ∈ ℂ → ( - 1 · 𝐴 ) = - 𝐴 )
3	1 2	ax-mp	⊢ ( - 1 · 𝐴 ) = - 𝐴