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 ⊢ φ → A ∈ ℝ
remulneg2d.b ⊢ φ → B ∈ ℝ
Assertion remulneg2d ⊢ φ → A ⁢ 0 - ℝ B = 0 - ℝ A ⁢ B

Proof

Step Hyp Ref Expression
1 remulneg2d.a ⊢ φ → A ∈ ℝ
2 remulneg2d.b ⊢ φ → B ∈ ℝ
3 0red ⊢ φ → 0 ∈ ℝ
4 resubdi ⊢ A ∈ ℝ ∧ 0 ∈ ℝ ∧ B ∈ ℝ → A ⁢ 0 - ℝ B = A ⋅ 0 - ℝ A ⁢ B
5 1 3 2 4 syl3anc ⊢ φ → A ⁢ 0 - ℝ B = A ⋅ 0 - ℝ A ⁢ B
6 remul01 ⊢ A ∈ ℝ → A ⋅ 0 = 0
7 1 6 syl ⊢ φ → A ⋅ 0 = 0
8 7 oveq1d ⊢ φ → A ⋅ 0 - ℝ A ⁢ B = 0 - ℝ A ⁢ B
9 5 8 eqtrd ⊢ φ → A ⁢ 0 - ℝ B = 0 - ℝ A ⁢ B