Metamath Proof Explorer


Theorem mulneg1i

Description: Product with negative is negative of product. Theorem I.12 of Apostol p. 18. (Contributed by NM, 10-Feb-1995) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulm1.1 A
mulneg.2 B
Assertion mulneg1i A B = A B

Proof

Step Hyp Ref Expression
1 mulm1.1 A
2 mulneg.2 B
3 mulneg1 A B A B = A B
4 1 2 3 mp2an A B = A B