Metamath Proof Explorer


Theorem remulneg2d

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

Ref Expression
Hypotheses remulneg2d.a ( 𝜑𝐴 ∈ ℝ )
remulneg2d.b ( 𝜑𝐵 ∈ ℝ )
Assertion remulneg2d ( 𝜑 → ( 𝐴 · ( 0 − 𝐵 ) ) = ( 0 − ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 remulneg2d.a ( 𝜑𝐴 ∈ ℝ )
2 remulneg2d.b ( 𝜑𝐵 ∈ ℝ )
3 0red ( 𝜑 → 0 ∈ ℝ )
4 resubdi ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · ( 0 − 𝐵 ) ) = ( ( 𝐴 · 0 ) − ( 𝐴 · 𝐵 ) ) )
5 1 3 2 4 syl3anc ( 𝜑 → ( 𝐴 · ( 0 − 𝐵 ) ) = ( ( 𝐴 · 0 ) − ( 𝐴 · 𝐵 ) ) )
6 remul01 ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
7 1 6 syl ( 𝜑 → ( 𝐴 · 0 ) = 0 )
8 7 oveq1d ( 𝜑 → ( ( 𝐴 · 0 ) − ( 𝐴 · 𝐵 ) ) = ( 0 − ( 𝐴 · 𝐵 ) ) )
9 5 8 eqtrd ( 𝜑 → ( 𝐴 · ( 0 − 𝐵 ) ) = ( 0 − ( 𝐴 · 𝐵 ) ) )