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

Metamath Proof Explorer

Theorem cjmul

Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjmul ⊢ 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 simp3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ‾ = A ‾ ⁢ B ‾