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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
2 mulneg12 ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · - - 𝐵 ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · - - 𝐵 ) )
4 negneg ⊢ ( 𝐵 ∈ ℂ → - - 𝐵 = 𝐵 )
5 4 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - - 𝐵 = 𝐵 )
6 5 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · - - 𝐵 ) = ( 𝐴 · 𝐵 ) )
7 3 6 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · 𝐵 ) )