This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem remulneg2d

Description: Product with negative is negative of product. (Contributed by SN, 25-Jan-2025)

Ref Expression
Hypotheses remulneg2d.a 
|- ( ph -> A e. RR )
remulneg2d.b 
|- ( ph -> B e. RR )
Assertion remulneg2d 
|- ( ph -> ( A x. ( 0 -R B ) ) = ( 0 -R ( A x. B ) ) )

Proof

Step Hyp Ref Expression
1 remulneg2d.a 
 |-  ( ph -> A e. RR )
2 remulneg2d.b 
 |-  ( ph -> B e. RR )
3 0red 
 |-  ( ph -> 0 e. RR )
4 resubdi 
 |-  ( ( A e. RR /\ 0 e. RR /\ B e. RR ) -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) )
5 1 3 2 4 syl3anc 
 |-  ( ph -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) )
6 remul01 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
7 1 6 syl 
 |-  ( ph -> ( A x. 0 ) = 0 )
8 7 oveq1d 
 |-  ( ph -> ( ( A x. 0 ) -R ( A x. B ) ) = ( 0 -R ( A x. B ) ) )
9 5 8 eqtrd 
 |-  ( ph -> ( A x. ( 0 -R B ) ) = ( 0 -R ( A x. B ) ) )