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

Metamath Proof Explorer

Theorem addmulsub

Description: The product of a sum and a difference. (Contributed by AV, 5-Mar-2023)

Ref Expression
Assertion addmulsub ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C − D = A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ∈ ℂ
2 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B ∈ ℂ
3 1 2 addcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ∈ ℂ
4 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C ∈ ℂ
5 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → D ∈ ℂ
6 3 4 5 subdid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C − D = A + B ⁢ C − A + B ⁢ D
7 1 2 4 adddird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C = A ⁢ C + B ⁢ C
8 1 2 5 adddird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ D = A ⁢ D + B ⁢ D
9 7 8 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C − A + B ⁢ D = A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D
10 6 9 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C − D = A ⁢ C + B ⁢ C - A ⁢ D + B ⁢ D