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

Metamath Proof Explorer

Theorem muladdi

Description: Product of two sums. (Contributed by NM, 17-May-1999)

Ref Expression
Hypotheses mulm1.1 ⊢ A ∈ ℂ
mulneg.2 ⊢ B ∈ ℂ
subdi.3 ⊢ C ∈ ℂ
muladdi.4 ⊢ D ∈ ℂ
Assertion muladdi ⊢ A + B ⁢ C + D = A ⁢ C + D ⁢ B + A ⁢ D + C ⁢ B

Proof

Step Hyp Ref Expression
1 mulm1.1 ⊢ A ∈ ℂ
2 mulneg.2 ⊢ B ∈ ℂ
3 subdi.3 ⊢ C ∈ ℂ
4 muladdi.4 ⊢ D ∈ ℂ
5 muladd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ⁢ C + D = A ⁢ C + D ⁢ B + A ⁢ D + C ⁢ B
6 1 2 3 4 5 mp4an ⊢ A + B ⁢ C + D = A ⁢ C + D ⁢ B + A ⁢ D + C ⁢ B