Complex Conjugate Root Theorem

Complex Conjugate Root Theorem states that for a real coefficient polynomial $P(x)$, if $a+bi$ (where $i$ is the imaginary unit) is a root of $P(x)$, then so is $a-bi$

To prove this, we need some lemma first.

Let $x=a+bi,y=c+di \in \mathbb C$.
Let $\overline \cdot$ denote the conjugate of a complex number.
$\overline{x+y}=\overline{a+bi+c+di}=\overline{(a+c)+(b+d)i}=(a+c)-(b+d)i$
$\overline x + \overline y=\overline{a+bi} + \overline{c+di}=a-bi+c-di=(a+c)-(b+d)i$
$\square$

Let $x=a+bi,y=c+di \in \mathbb C$.
Let $\overline \cdot$ denote the conjugate of a complex number.
$\overline{xy}=\overline{(a+bi)(c+di)}=\overline{(ac-bd)+(bc+ad)i}=(ac-bd)-(bc+ad)i$
$(\overline x) (\overline y)=(\overline{a+bi})(\overline{c+di})=(a-bi)(c-di)=(ac-bd)-(bc+ad)i$
$\square$

This is immediate from Lemma $2$.

Let $\displaystyle P(x)=\sum_{i=0}^n a_i x^i$.
Let $z$ be a root of $P(x)$, i.e. $P(z)=0$ (by factor theorem).
Then,
$\;\;\;\;P(\overline z)$
$\displaystyle=\sum_{i=0}^n a_i \overline z^i$
$\displaystyle=\sum_{i=0}^n (\overline{a_i}) (\overline z^i)$ (real coefficients)
$\displaystyle=\sum_{i=0}^n (\overline{a_i}) (\overline{z^i})$ (Lemma $3$)
$\displaystyle=\sum_{i=0}^n (\overline{a_i z^i})$ (Lemma $2$)
$\displaystyle=\overline{\sum_{i=0}^n a_i z^i}$ (Lemma $1$)
$=\overline{P(z)}$
$=\overline 0$
$=0$
By factor theorem, $\overline z$ is also a root.
$\blacksquare$