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 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท ๐ต ) )