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

Metamath Proof Explorer

Theorem addneg1mul

Description: Addition with product with minus one is a subtraction. (Contributed by AV, 18-Oct-2021)

Ref Expression
Assertion addneg1mul ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + -1 ⁢ B = A − B

Proof

Step Hyp Ref Expression
1 mulm1 ⊢ B ∈ ℂ → -1 ⁢ B = − B
2 1 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → -1 ⁢ B = − B
3 2 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + -1 ⁢ B = A + − B
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 3 4 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + -1 ⁢ B = A − B