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 ) ) )