Proof of Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums

Each result cited is universally quantified over the data in its own statement.

The ring identities of Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, in $\mathbb{R}$ and in $\mathbb{C}$, are used throughout without further mention. Throughout, $\mathbb{C}$ is a field by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §complex, real numbers are elements of $\mathbb{C}$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §identification, sums, products, negatives, differences, reciprocals, quotients and powers of real numbers agree in $\mathbb{R}$ and in $\mathbb{C}$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §agreement, and $i^{2}=-1$ by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §canonical; in $\mathbb{R}$ and in $\mathbb{C}$, $x^{2}=x\cdot x$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product. Let $p,q,r,s,t\in\mathbb{R}$ and $u\in\mathbb{C}$. By Real and Imaginary Parts of a Complex Number §parts and the uniqueness in The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §canonical, $u=\operatorname{Re}u+(\operatorname{Im}u)\,i$, and $\operatorname{Re}(p+qi)=p$ and $\operatorname{Im}(p+qi)=q$. As $p=p+0\,i$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero, $\operatorname{Re}p=p$ and $\operatorname{Im}p=0$; conversely, if $\operatorname{Im}u=0$, then $u=\operatorname{Re}u+0\,i=\operatorname{Re}u\in\mathbb{R}$. So $u\in\mathbb{R}$ if and only if $\operatorname{Im}u=0$. The commutative ring axioms of $\mathbb{C}$, $i^{2}=-1$ and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs give the arithmetic rules

$$(p+qi)+(r+si)=(p+r)+(q+s)i,\quad -(p+qi)=(-p)+(-q)i,\quad t(p+qi)=tp+(tq)i,\quad (p+qi)(r+si)=(pr-qs)+(ps+qr)i,$$

and $\overline{u}=\operatorname{Re}u+(-\operatorname{Im}u)\,i$ by The Complex Conjugate of a Complex Number §conjugate and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, so $\operatorname{Re}\overline{u}=\operatorname{Re}u$ and $\operatorname{Im}\overline{u}=-\operatorname{Im}u$. Write $a=\operatorname{Re}z$, $b=\operatorname{Im}z$, $c=\operatorname{Re}w$ and $d=\operatorname{Im}w$.

Clause conjugation. By the arithmetic rules $z+w=(a+c)+(b+d)i$, so $\overline{z+w}=(a+c)+(-(b+d))i=(a+(-b)i)+(c+(-d)i)=\overline{z}+\overline{w}$, as $-(b+d)=(-b)+(-d)$. Likewise $zw=(ac-bd)+(ad+bc)i$, so $\overline{zw}=(ac-bd)+(-(ad+bc))i$, while $\overline{z}\,\overline{w}=(a+(-b)i)(c+(-d)i)=(ac-(-b)(-d))+(a(-d)+(-b)c)i$, which is the same number. Next, $\overline{\overline{z}}=a+(-(-b))i=a+bi=z$. Finally, $\overline{z}=z$ means $a+(-b)i=a+bi$, which by the uniqueness of imaginary parts holds if and only if $-b=b$; adding $b$ to both sides, this holds if and only if $b+b=0$, that is $2b=0$, and as $2\neq0$ in $\mathbb{R}$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §halving, this holds if and only if $b=0$; and $b=0$ if and only if $z\in\mathbb{R}$.

Clause parts. The arithmetic rules give $z+w=(a+c)+(b+d)i$ and $\lambda z=\lambda a+(\lambda b)i$, whence the four identities. Further $z+\overline{z}=(a+bi)+(a+(-b)i)=(a+a)+(b+(-b))i=2a+0\,i=2a$, and, since $-\overline{z}=(-a)+(-(-b))i=(-a)+bi$ by the arithmetic rules, $z-\overline{z}=(a+(-a))+(b+b)i=0+(2b)i=(2b)i$.

Clause modulus. By The Modulus of a Complex Number §modulus and The k-th Root and the Square Root of a Nonnegative Real Number §root, $|z|\ge0$, and $|z|^{2}=a^{2}+b^{2}$ by Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §power. The arithmetic rules give $z\overline{z}=(a+bi)(a+(-b)i)=(aa-b(-b))+(a(-b)+ba)i=(a^{2}+b^{2})+0\,i=a^{2}+b^{2}$, so $z\overline{z}=|z|^{2}=a^{2}+b^{2}$. If $z=0$, then $a=b=0$ as $0\in\mathbb{R}$, so $|z|=\sqrt{0}=0$ by Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §power. If $|z|=0$, then $a^{2}+b^{2}=0$; as $0\le a^{2}$ and $0\le b^{2}$, we get $0\le a^{2}\le a^{2}+b^{2}=0$, so $a\cdot a=0$ and $a=0$, likewise $b=0$, and $z=0+0\,i=0$. Since $\operatorname{Re}\overline{z}=a$, $\operatorname{Im}\overline{z}=-b$ and $-z=(-a)+(-b)i$ by the arithmetic rules, and $(-a)^{2}=a^{2}$ and $(-b)^{2}=b^{2}$, The Modulus of a Complex Number §modulus gives $|\overline{z}|=|-z|=\sqrt{a^{2}+b^{2}}=|z|$.

Clause multiplicative. By the clauses modulus and conjugation, the ring axioms of $\mathbb{C}$ and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product, $|zw|^{2}=(zw)\,\overline{zw}=(z\overline{z})(w\overline{w})=|z|^{2}|w|^{2}=(|z|\,|w|)^{2}$. Both $|zw|$ and $|z|\,|w|$ are $\ge0$ by the clause modulus, so they are equal by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff with $n=2$.

Clause inverse. Let $z\neq0$. Then $|z|\neq0$ by the clause modulus, so $|z|^{2}\neq0$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §reciprocal, and $z\cdot\big(\overline{z}\,(|z|^{2})^{-1}\big)=(z\overline{z})(|z|^{2})^{-1}=|z|^{2}(|z|^{2})^{-1}=1$ by the clause modulus; hence $z^{-1}=\overline{z}/|z|^{2}$ by Additive and Multiplicative Inverses Are Unique §reciprocal. As $\operatorname{Re}1=1$ and $\operatorname{Im}1=0$, $|1|=\sqrt{1}=1$ by Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §power, so $|z|\,|z^{-1}|=|zz^{-1}|=1$ by the clause multiplicative, and $|z^{-1}|=1/|z|$ by Additive and Multiplicative Inverses Are Unique §reciprocal applied in $\mathbb{R}$.

Clause components. Since $0\le b^{2}$, $a^{2}\le a^{2}+b^{2}$, so, reading the modulus of the real numbers $a$ and $b$ as their absolute values by The Modulus of a Complex Number §agreement, $|a|=\sqrt{a^{2}}\le\sqrt{a^{2}+b^{2}}=|z|$ by Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §abs and Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §monotone; likewise $|b|\le|z|$. By Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §subadditive and Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §abs, $|z|=\sqrt{a^{2}+b^{2}}\le\sqrt{a^{2}}+\sqrt{b^{2}}=|a|+|b|$.

Clause triangle. Let $v=z\overline{w}$; then $\overline{v}=\overline{z}\,w$ by the clause conjugation. By the clauses conjugation, modulus and parts and the ring axioms of $\mathbb{C}$,

$$|z+w|^{2}=(z+w)(\overline{z}+\overline{w})=z\overline{z}+w\overline{w}+v+\overline{v}=|z|^{2}+|w|^{2}+2\operatorname{Re}v.$$

Now $\operatorname{Re}v\le|\operatorname{Re}v|\le|v|=|z|\,|\overline{w}|=|z|\,|w|$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value, The Modulus of a Complex Number §agreement and the clauses components, multiplicative and modulus, so $|z+w|^{2}\le|z|^{2}+2|z|\,|w|+|w|^{2}=(|z|+|w|)^{2}$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §squares. As $|z+w|\ge0$ and $|z|+|w|\ge0$, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff with $n=2$ gives $|z+w|\le|z|+|w|$. Applied to $z-w$ and $w$, this gives $|z|=|(z-w)+w|\le|z-w|+|w|$, so $|z|-|w|\le|z-w|$; symmetrically $|w|-|z|\le|w-z|=|-(z-w)|=|z-w|$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs and the clause modulus. Thus $-|z-w|\le|z|-|w|\le|z-w|$, and $\big||z|-|w|\big|\le|z-w|$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value, the outer modulus of the real number $|z|-|w|$ being its absolute value by The Modulus of a Complex Number §agreement.

Clause sums. Addition on $\mathbb{C}$ and on $\mathbb{R}$ is associative and commutative with neutral element $0$, and finite sums in $\mathbb{C}$ are as in The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers §complex. The map $u\mapsto\overline{u}$ from $\mathbb{C}$ to $\mathbb{C}$ sends $0$ to $0$, as $0\in\mathbb{R}$, and sums to sums, by the clause conjugation; the maps $\operatorname{Re}$ and $\operatorname{Im}$ from $\mathbb{C}$ to $\mathbb{R}$ send $0$ to $0$, as $0\in\mathbb{R}$, and sums to sums, by the clause parts. So Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §homomorphism gives the three identities. Let $S=\sum_{x\in A}f(x)$. As $|f(x)|\ge0$ for every $x\in A$ by the clause modulus, $0\le\sum_{x\in A}|f(x)|$ by Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §monotone, which settles the case $S=0$, where $|S|=0$ by the clause modulus. Let $S\neq0$, so $|S|>0$ by the clause modulus. By the clause modulus and Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §distributive, $|S|^{2}=\overline{S}\,S=\sum_{x\in A}\overline{S}f(x)$. As $|S|^{2}$ is real, it equals its real part; so by the identity for $\operatorname{Re}$ just proved, the bound $\operatorname{Re}v\le|\operatorname{Re}v|\le|v|$ for $v\in\mathbb{C}$ from Rules of Arithmetic and Order in an Ordered Field §absolute-value, The Modulus of a Complex Number §agreement and the clause components, Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §comparison, the clauses multiplicative and modulus, and Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality §distributive,

$$|S|^{2}=\sum_{x\in A}\operatorname{Re}\big(\overline{S}f(x)\big)\le\sum_{x\in A}\big|\overline{S}f(x)\big|=\sum_{x\in A}|S|\,|f(x)|=|S|\sum_{x\in A}|f(x)|.$$

Since $|S|^{2}=|S|\cdot|S|$ and $|S|>0$, Rules of Arithmetic and Order in an Ordered Field §order-product gives $|S|\le\sum_{x\in A}|f(x)|$.