Conjugation is an involutive real-field automorphism, $z\bar{z}=\mathrm{\mid }z{\mathrm{\mid }}^2$, and modulus is definite, multiplicative, and subadditive

Coordinate expansion using [F1] and [F2] proves the two homomorphism laws, that conjugation fixes every real number, and that applying it twice is the identity. Thus conjugation is an involutive real-field automorphism.

Direct multiplication gives $z\bar{z}=a^2+b^2=\mathrm{\mid }z{\mathrm{\mid }}^2$.

Lagrange's identity gives $(a^2+b^2)(u^2+v^2)-(au+bv{)}^2=(av-bu{)}^2\ge 0.$ The final inequality follows from [F5], with the zero case included.

By [F2] and [F3], $\mathrm{\mid }z\mathrm{\mid }\ge 0$. If $z=0$, then $\mathrm{\mid }z\mathrm{\mid }=0$; conversely, $\mathrm{\mid }z\mathrm{\mid }=0$ makes $a^2+b^2=0$, and [F5] forces $a=b=0$.

Apply step 1.2 to $zw$ and use step 1.1: $\mathrm{\mid }zw{\mathrm{\mid }}^2=(zw)\overline{zw}=(z\bar{z})(w\bar{w})=\mathrm{\mid }z{\mathrm{\mid }}^2\mathrm{\mid }w{\mathrm{\mid }}^2$. Both sides of $\mathrm{\mid }zw\mathrm{\mid }=\mathrm{\mid }z\mathrm{\mid }\mathrm{\mid }w\mathrm{\mid }$ are nonnegative, so uniqueness in [F3] proves multiplicativity.

Hence $au+bv\le \mathrm{\mid }z\mathrm{\mid }\mathrm{\mid }w\mathrm{\mid }$: if $au+bv\le 0$ this follows from $\mathrm{\mid }z\mathrm{\mid }\mathrm{\mid }w\mathrm{\mid }\ge 0$; otherwise both quantities are nonnegative, step 1.3 and [F4] give the inequality after squaring.

Expanding with [F1] and [F2], then using step 3.2, gives $\mathrm{\mid }z+w{\mathrm{\mid }}^2=a^2+b^2+u^2+v^2+2(au+bv)\le (\mathrm{\mid }z\mathrm{\mid }+\mathrm{\mid }w\mathrm{\mid }{)}^2\mathrm{.}$

Both sides of $\mathrm{\mid }z+w\mathrm{\mid }\le \mathrm{\mid }z\mathrm{\mid }+\mathrm{\mid }w\mathrm{\mid }$ are nonnegative, so [F4] turns the squared inequality in step 4.1 into the triangle inequality.