Metamath Proof Explorer


Theorem mulneg2

Description: The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004)

Ref Expression
Assertion mulneg2 ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - ๐ต ) = - ( ๐ด ยท ๐ต ) )

Proof

Step Hyp Ref Expression
1 mulneg1 โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( - ๐ต ยท ๐ด ) = - ( ๐ต ยท ๐ด ) )
2 1 ancoms โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( - ๐ต ยท ๐ด ) = - ( ๐ต ยท ๐ด ) )
3 negcl โŠข ( ๐ต โˆˆ โ„‚ โ†’ - ๐ต โˆˆ โ„‚ )
4 mulcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง - ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - ๐ต ) = ( - ๐ต ยท ๐ด ) )
5 3 4 sylan2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - ๐ต ) = ( - ๐ต ยท ๐ด ) )
6 mulcom โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ต ) = ( ๐ต ยท ๐ด ) )
7 6 negeqd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ - ( ๐ด ยท ๐ต ) = - ( ๐ต ยท ๐ด ) )
8 2 5 7 3eqtr4d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - ๐ต ) = - ( ๐ด ยท ๐ต ) )