ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2413 on D507: Complex conjugate
Complex conjugate of real number
Formulation 0
Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.
Then \begin{equation} y = 0 \quad \iff \quad \overline{z} = z \end{equation}
Proofs
Proof 0
Let $z = (x, y) \in \mathbb{C}$ be a D1207: Complex number.
The complex conjugate $\overline{z}$ is defined as $\overline{z} = (x, - y)$. If $y = 0$, then result R4483: Real number is zero iff equal to its reflection shows that $y = - y$ and we have \begin{equation} \overline{z} = (x, - y) = (x, y) = z \end{equation} Conversely, assume that $\overline{z} = z$ holds. Then \begin{equation} (x, - y) = \overline{z} = z = (x, y) \end{equation} whence result R3346: Characterisation of equality of ordered pairs states that $x = x$ and, in particular, $- y = y$. Result R4483: Real number is zero iff equal to its reflection now shows that $y = 0$. $\square$