ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4706 on D507: Complex conjugate

Complex conjugate zero iff argument zero

Formulation 0

Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.

Then \begin{equation} \overline{z} = (0, 0) \quad \iff \quad z = (0, 0) \end{equation}

Formulation 1

Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.

Then \begin{equation} \overline{z} = 0 \quad \iff \quad z = 0 \end{equation}

Proofs

Proof 0

Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.

Suppose first that $\overline{z} = \overline{(x, y)} = (0, 0)$. Since $(0, 0)$ has its second component zero, then results

(i)	R2950: Complex conjugation operation is an involution
(ii)	R2413: Complex conjugate of real number

imply \begin{equation} z = \overline{\overline{z}} = \overline{(0, 0)} = (0, 0) \end{equation} Conversely, assume that $z = (0, 0)$. Then result R2413: Complex conjugate of real number immediately implies $\overline{z} = \overline{(0, 0)} = (0, 0)$. $\square$