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

Metamath Proof Explorer

Theorem remuli

Description: Real part of a product. (Contributed by NM, 28-Jul-1999)

Ref Expression
Hypotheses recl.1 ⊢ A ∈ ℂ
readdi.2 ⊢ B ∈ ℂ
Assertion remuli ⊢ ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B

Proof

Step Hyp Ref Expression
1 recl.1 ⊢ A ∈ ℂ
2 readdi.2 ⊢ B ∈ ℂ
3 remul ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B
4 1 2 3 mp2an ⊢ ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B