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

Metamath Proof Explorer

Theorem mul2neg

Description: Product of two negatives. Theorem I.12 of Apostol p. 18. (Contributed by NM, 30-Jul-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion mul2neg ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ − B = A ⁢ B

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 mulneg12 ⊢ A ∈ ℂ ∧ − B ∈ ℂ → − A ⁢ − B = A ⁢ − − B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ − B = A ⁢ − − B
4 negneg ⊢ B ∈ ℂ → − − B = B
5 4 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − B = B
6 5 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ − − B = A ⁢ B
7 3 6 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ − B = A ⁢ B