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 ABAB=AB

Proof

Step Hyp Ref Expression
1 negcl BB
2 mulneg12 ABAB=AB
3 1 2 sylan2 ABAB=AB
4 negneg BB=B
5 4 adantl ABB=B
6 5 oveq2d ABAB=AB
7 3 6 eqtrd ABAB=AB