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

Metamath Proof Explorer

Theorem immul

Description: Imaginary part of a product. (Contributed by NM, 28-Jul-1999) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion immul ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B

Proof

Step Hyp Ref Expression
1 remullem ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B ∧ ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B ∧ A ⁢ B ‾ = A ‾ ⁢ B ‾
2 1 simp2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B