ThmDex – An index of mathematical definitions, results, and conjectures.
Result R5297 on D507: Complex conjugate
Complex conjugate of a product of two complex numbers
Formulation 0
Let $z, w \in \mathbb{C}$ each be a D1207: Complex number.
Then \begin{equation} \overline{z w} = \overline{z} \, \overline{w} \end{equation}
Proofs
Proof 0
Let $z, w \in \mathbb{C}$ each be a D1207: Complex number.
Denote $z = (a, b)$ and $w = (c, d)$. Using the definitions
(i) D611: Complex multiplication operation
(ii) D507: Complex conjugate

we have \begin{equation} \begin{split} \overline{z w} = \overline{(a, b) (c, d)} & = \overline{(a c - b d, a d + b c)} \\ & = (a c - b d, - a d -b c) \\ & = (a, -b)(c, -d) \\ & = \overline{(a, b)} \overline{(c, d)} \\ & = \overline{z} \, \overline{w} \end{split} \end{equation} $\square$