Proof of Properties of Complex Conjugation and Modulus

Write $a=\operatorname{Re}z$, $b=\operatorname{Im}z$, $c=\operatorname{Re}w$, $d=\operatorname{Im}w$, so that $z=a+bi$ and $w=c+di$ are the canonical representations given by claim 3 of Canonical Form and Arithmetic of Complex Numbers and the definition of real and imaginary parts. All computations in canonical form use claim 4 of Canonical Form and Arithmetic of Complex Numbers, and all statements about identities and inverses of real numbers inside $\mathbb{C}$ use claim 1 of the same lemma. By definition $\overline{z}=a+(-b)i$, and by definition $|z|$ is the unique real number with $0\le|z|$ and $|z|^{2}=a^{2}+b^{2}$. Since $\mathbb{R}$ is an ordered field by The Real Numbers, we use its field axioms, the two order-compatibility conditions, and the properties of the total order. As in the statement, $2x$ abbreviates $x+x$ and $x^{2}$ abbreviates $x\cdot x$ for real $x$.

Step 0 (three facts about real numbers).

(i) If $u\le v$ and $0\le t$, then $ut\le vt$. Indeed, adding $-u$ to $u\le v$ gives $0\le v+(-u)$, so $0\le(v+(-u))t=vt+(-(ut))$ by the second order-compatibility condition and the identity $x\cdot(-y)=-(x\cdot y)$; adding $ut$ gives $ut\le vt$.

(ii) If $0\le x$, $0\le y$ and $x^{2}\le y^{2}$, then $x\le y$; and if $0\le x$, $0\le y$ and $x^{2}=y^{2}$, then $x=y$. For the second assertion, $x$ and $y$ are both nonnegative real numbers whose square is the same nonnegative real number, so they are equal by Existence and Uniqueness of the Nonnegative Square Root. For the first, suppose $x\le y$ fails. Since the order is total, $y\le x$ and $y\neq x$. By (i), $y\cdot y\le x\cdot y$ and $x\cdot y\le x\cdot x$, so $y^{2}\le x^{2}$; with $x^{2}\le y^{2}$ and antisymmetry, $x^{2}=y^{2}$, whence $x=y$ by the second assertion, a contradiction.

(iii) If $x$ is real and $x+x=0$, then $x=0$. If $0\le x$, adding $x$ to both sides gives $x\le x+x=0$, so $x=0$ by antisymmetry; if $x\le0$, adding $x$ gives $0=x+x\le x$, so again $x=0$.

Claim 1. By claim 4 of Canonical Form and Arithmetic of Complex Numbers,

and these are canonical representations, so $\overline{z+w}=(a+c)+(-(b+d))i=\bigl(a+(-b)i\bigr)+\bigl(c+(-d)i\bigr)=\overline{z}+\overline{w}$. Similarly

Also $\overline{\overline{z}}=a+(-(-b))i=a+bi=z$. Finally, $\overline{z}=z$ means $a+(-b)i=a+bi$, which by uniqueness of the canonical representation means $-b=b$, i.e. $b+b=0$, i.e. $b=0$ by Step 0(iii); and $b=0$ holds if and only if $z=a\in\mathbb{R}$, since conversely every real $x$ has canonical representation $x+0i$ and hence imaginary part $0$.

Claim 2. $z+\overline{z}=(a+a)+(b+(-b))i=2a=2\operatorname{Re}z$ and $z-\overline{z}=(a+(-a))+(b+b)i=(2b)i=(2\operatorname{Im}z)i$.

Claim 3. By claim 4 of Canonical Form and Arithmetic of Complex Numbers,

The real and imaginary parts of $\overline{z}$ are $a$ and $-b$, so $|\overline{z}|$ is the nonnegative real number with $|\overline{z}|^{2}=a^{2}+(-b)^{2}=a^{2}+b^{2}=|z|^{2}$; since $|z|$ and $|\overline{z}|$ are nonnegative with equal squares, $|\overline{z}|=|z|$ by Step 0(ii). If $|z|=0$ then $a^{2}+b^{2}=|z|^{2}=0$; since $0\le a^{2}$ and $0\le b^{2}$ by Existence and Uniqueness of the Square Root of a Sum of Two Squares applied to the pairs $a,0$ and $b,0$, adding $b^{2}$ to $0\le a^{2}$ gives $b^{2}\le a^{2}+b^{2}=0$, so $b^{2}=0$ and hence $b=0$ because a field has no zero divisors, and symmetrically $a=0$; thus $z=0$. Conversely, if $z=0$ then $a=b=0$, so $|z|^{2}=0$ and therefore $|z|=0$, again because a field has no zero divisors.

Claim 4. Using claim 4 of Canonical Form and Arithmetic of Complex Numbers and expanding in $\mathbb{R}$,

the cross terms cancelling. Both $|zw|$ and $|z||w|$ are nonnegative, the latter by the second order-compatibility condition applied to $0\le|z|$ and $0\le|w|$, so $|zw|=|z||w|$ by Step 0(ii).

Claim 5. Let $z\neq0$. By claim 3, $|z|\neq0$, so $|z|^{2}\neq0$ and the real number $|z|^{-2}=1/|z|^{2}$ exists; by claim 1 of Canonical Form and Arithmetic of Complex Numbers it is also the multiplicative inverse of $|z|^{2}$ in $\mathbb{C}$. Using commutativity and associativity of multiplication in $\mathbb{C}$ and claim 3,

Since multiplicative inverses in a field are unique, $z^{-1}=|z|^{-2}\overline{z}$.

Claim 6. By Existence and Uniqueness of the Square Root of a Sum of Two Squares applied to $b$ and $0$ we have $0\le b^{2}$, so adding $a^{2}$ gives $a^{2}\le a^{2}+b^{2}=|z|^{2}$. If $a\le0$, then $a\le0\le|z|$ by transitivity. If $0\le a$, then $a\le|z|$ by Step 0(ii). The same argument applied to $-a$, using $(-a)^{2}=a^{2}$, gives $-a\le|z|$; and the argument with $b$ and $-b$ in place of $a$, using $b^{2}\le a^{2}+b^{2}$, gives $b\le|z|$ and $-b\le|z|$.

Claim 7. Expanding in $\mathbb{R}$,

By claim 4 of Canonical Form and Arithmetic of Complex Numbers, $z\overline{w}=(ac+bd)+(bc-ad)i$, so $ac+bd=\operatorname{Re}(z\overline{w})$. By claim 6 applied to $z\overline{w}$, then claim 4 and claim 3,

Adding this inequality to itself, which is permitted by the first order-compatibility condition applied twice, gives $2(ac+bd)\le2|z||w|$; adding $|z|^{2}+|w|^{2}$ to both sides gives

Both $|z+w|$ and $|z|+|w|$ are nonnegative, the latter because adding $|w|$ to $0\le|z|$ gives $|w|\le|z|+|w|$, and $0\le|w|$. Hence $|z+w|\le|z|+|w|$ by Step 0(ii).

Claim 8. Let $x\in\mathbb{R}$. Its canonical representation is $x+0i$, so $|x|$ is the nonnegative real number with $|x|^{2}=x^{2}+0^{2}=x^{2}$. If $0\le x$, then $x$ is nonnegative with $x^{2}=|x|^{2}$, so $|x|=x$ by Step 0(ii). Otherwise, since the order is total, $x\le0$, so $0\le-x$ and $(-x)^{2}=x^{2}=|x|^{2}$, whence $|x|=-x$ by Step 0(ii).

Claim 9. We verify the four conditions of Metric Space for $d_{\mathbb{C}}(z,w)=|z-w|$, which is a real number for every pair of complex numbers $z,w$. Condition 1, $0\le|z-w|$, holds by the definition of the modulus. Condition 2: by claim 3, $|z-w|=0$ if and only if $z-w=0$, that is, if and only if $z=w$. Condition 3: $w-z=(-1)(z-w)$ by the field identities $(-1)x=-x$ and $-(x+y)=(-x)+(-y)$, so by claim 4 and claim 8, $|w-z|=|-1|\,|z-w|=1\cdot|z-w|=|z-w|$. Condition 4: for complex $z,w,u$ we have $z-u=(z-w)+(w-u)$, so claim 7 gives $|z-u|\le|z-w|+|w-u|$. Hence $d_{\mathbb{C}}$ is a metric on $\mathbb{C}$.