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 −ℝ ( 𝐴 · 𝐵 ) ) ) |
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 −ℝ ( 𝐴 · 𝐵 ) ) ) |