This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulm1

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

Ref Expression
Assertion mulm1 ⊢ A ∈ ℂ → -1 ⁢ A = − A

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 mulneg1 ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → -1 ⁢ A = − 1 ⁢ A
3 1 2 mpan ⊢ A ∈ ℂ → -1 ⁢ A = − 1 ⁢ A
4 mullid ⊢ A ∈ ℂ → 1 ⁢ A = A
5 4 negeqd ⊢ A ∈ ℂ → − 1 ⁢ A = − A
6 3 5 eqtrd ⊢ A ∈ ℂ → -1 ⁢ A = − A