Complex modulus and conjugate: proving z·z̄=|z|² and that conjugation preserves the operations

Goal and scope

For z=a+bi and w=c+di (a, b, c, d real) prove: (1) z·z̄=(a²+b²)+0i, the real embedding of the modulus squared; (2) conjugation preserves addition: (z+w)‾=z̄+w̄; (3) conjugation preserves multiplication: (zw)‾=z̄·w̄; (4) hence |zw|²=|z|²|w|². Then check everything exactly for z=3−4i and w=1+2i, distinguishing the modulus squared from the modulus.

The general proofs hold for real components; the examples use integer ordered pairs (MKO assumption a1) and compute only conjugates and modulus squares, without passing off decimal square-root approximations as exact moduli. Only where |z|²=25 is a perfect square is |z|=5 stated. Arguments, polar form and complex differentiability are not treated (MKO assumption a2); the canonical MKO and its English edition are not changed.

Givens and symbols

• mul_assoc
• mul_comm
• neg_mul
• square_nonneg
• numeric_evaluation

• G1 — General case: z=a+bi corresponds to (a,b) and w=c+di to (c,d), with a, b, c, d real.
• G2 — Example: z=3−4i corresponds to (3,−4) and w=1+2i to (1,2).
• G3 — Answers are exact integers or ordered pairs; a modulus squared that is not a perfect square is kept as it is, with no decimal approximation (MKO assumption a1).

• z=a+bi\leftrightarrow(a,b) — a complex number and its ordered pair
• \overline{z}=a-bi — the conjugate of z
• |z|^2=a^2+b^2 — the modulus squared of z
• |z|=\sqrt{a^2+b^2} — the modulus of z (nonnegative square root)
• w=c+di — the second complex number

Rules and sources

• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• mko_modconj_def · cited — For z=a+b*i, the conjugate is a−b*i and modulus squared is a²+b². Multiplying z by its conjugate gives the real embedding of that squared modulus. Conjugation preserves addition and multiplication. · mko-complex-modulus-conjugate
• complex_mul_formula · cited — Complex multiplication follows from distributivity and i²=−1: the product (a+bi)(c+di) has real part ac−bd and imaginary coefficient ad+bc. · mko-complex-number
• complex_addsub · prerequisite — Componentwise addition and subtraction: (a+bi)±(c+di)=(a±c)+(b±d)i.
• complex_pair_eq · prerequisite — For reals a, b, c, d: a+bi=c+di if and only if a=c and b=d.
• real_embedding · prerequisite — A real r is embedded as r+0i, the ordered pair (r,0); the product of two embedded reals is (r,0)(s,0)=(rs,0).
• modulus_def · prerequisite — The modulus |z| is the nonnegative square root of the modulus squared a²+b²: |z|=√(a²+b²).
• L_conj_mul · lemma — For all complex numbers z, w: (zw)‾=z̄·w̄.
• L_modsq_mul · lemma — For all complex numbers z, w: |zw|²=|z|²·|w|².

Main derivation

z=a+bi\leftrightarrow(a,b)

\overline{z}=a-bi\leftrightarrow(a,-b),\ |z|^2=a^2+b^2

z\overline{z}=(a,b)\cdot(a,-b)

(a^2+b^2,\,0)

z\overline{z}=(a^2+b^2,\,0)

z\overline{z}=|z|^2\in\mathbb{R},\ |z|^2\ge 0

\overline{z+w}=\overline{(a+c)+(b+d)i}

(a+c)-(b+d)i=(a-bi)+(c-di)=\overline{z}+\overline{w}

\overline{zw}

\overline{z}\cdot\overline{w}

|zw|^2

|z|^2\,|w|^2

z=3-4i\leftrightarrow(3,-4)

\overline{z}=3+4i\leftrightarrow(3,4)

|z|^2=3^2+(-4)^2,\ z\overline{z}=(3,-4)(3,4)

|z|^2=25,\ z\overline{z}=(3\cdot3-(-4)\cdot4,\,3\cdot4+(-4)\cdot3)=(25,0)

|z|^2=25

|z|=\sqrt{25}=5\neq 25

w=1+2i

\overline{w}=1-2i,\ |w|^2=5,\ |w|=\sqrt5\notin\mathbb{Z}

zw=(3,-4)(1,2)

(3\cdot1-(-4)\cdot2,\,3\cdot2+(-4)\cdot1)=(11,2)

\overline{zw}\ \text{vs}\ \overline{z}\,\overline{w}=(3,4)(1,-2)

(11,-2)=(3\cdot1-4\cdot(-2),\,3\cdot(-2)+4\cdot1)

|zw|^2=11^2+2^2

125=25\cdot5=|z|^2|w|^2

\overline{z+w}=\overline{(4,-2)}

(4,2)=(3,4)+(1,-2)=\overline{z}+\overline{w}

z=a+bi,\ w=c+di

z\overline{z}=(|z|^2,0),\ \overline{z+w}=\overline{z}+\overline{w},\ \overline{zw}=\overline{z}\,\overline{w},\ |zw|^2=|z|^2|w|^2

Substeps and lemmas

\operatorname{Re}(z\overline{z})=a\cdot a-b\cdot(-b)

a^2+b^2

\operatorname{Im}(z\overline{z})=a\cdot(-b)+b\cdot a

0

\overline{zw}=\overline{(ac-bd)+(ad+bc)i}

(ac-bd,\,-(ad+bc))

\overline{z}\cdot\overline{w}=(a,-b)\cdot(c,-d)

(ac-(-b)(-d),\,a(-d)+(-b)c)=(ac-bd,\,-(ad+bc))

(|zw|^2,0)=(zw)\,\overline{zw}

(zw)(\overline{z}\,\overline{w})=(z\overline{z})(w\overline{w})

(z\overline{z})(w\overline{w})=(|z|^2,0)(|w|^2,0)

(|z|^2|w|^2,\,0)\ \Rightarrow\ |zw|^2=|z|^2|w|^2

Reverse audits

• S15 · sufficient_goal_reduction · S03, S04, S05, S06, and_intro_elim — Goal G: the four general statements. Sufficient condition H: S03, S04, S05 and S06, each proved for arbitrary a, b, c, d; H⇒G by conjunction introduction. G is never used as a premise, and no example stands in for a proof.
• S14 · premise_audit · S04, complex_addsub, numeric_evaluation — An instance check; the general conclusion comes from S04.
• S13 · premise_audit · L_modsq_mul, numeric_evaluation — The instance only checks the computation (N17); the general conclusion comes from S06.
• S12 · premise_audit · S05, complex_mul_formula, numeric_evaluation — The instance only checks the computation (N15, N16); the general conclusion comes from S05.
• S11 · inverse_equivalence · complex_mul_formula, numeric_evaluation — Exact evaluation of the formula (N13, N14); both sides are the same number.
• S10 · premise_audit · mko_modconj_def, order_basics, numeric_evaluation — The non-square argument splits into n≤2 and n≥3, which cover all nonnegative integers; nothing further about √5 is claimed.
• S09 · premise_audit · modulus_def, sqrt_def, numeric_evaluation — It needs 25 to be a perfect square for the exact integer 5 to appear; this fails for w (S10).
• S08 · premise_audit · S02, complex_mul_formula, numeric_evaluation — This is one instance of the general theorem (N6 to N8), used to check the computation; it does not replace the proof in S02.
• S07 · inverse_equivalence · mko_modconj_def — Conjugating twice returns the number: the conjugate of (3,4) is (3,−4)=z.
• S06.2 · premise_audit · S03, real_embedding, complex_pair_eq — Comparing real parts uses equality of ordered pairs; the step takes the real part of the equation and claims nothing else.
• S06.1 · inverse_equivalence · S03, S05, mul_assoc, mul_comm — Replacement of equals and regrouping are equations; undoing them in order restores the original.
• S06 · inverse_equivalence · L_modsq_mul — Both sides are the same real number, so the step is two-way.
• S05.2 · inverse_equivalence · neg_mul, complex_pair_eq, distributive — The sign rules and distributivity are identities (checked on a grid in N3 and N4), so the step is two-way.
• S05.1 · inverse_equivalence · complex_mul_formula, mko_modconj_def — The formula and the definition of the conjugate are equations; conjugating again returns zw.
• S05 · inverse_equivalence · L_conj_mul — The lemma is an equation and both sides are the same complex number, so the step is two-way.
• S04 · inverse_equivalence · complex_addsub, complex_pair_eq, neg_mul — Each equals sign is an identity rewrite (−(b+d)=−b−d) and both components agree, so the step is two-way.
• S03 · premise_audit · S02, real_embedding, square_nonneg — Nonnegativity uses that squares are nonnegative; the step does not claim that every nonnegative real is the modulus squared of an integer pair.
• S02.2 · inverse_equivalence · mul_comm, neg_mul, add_inverse — An identity (N2), two-way.
• S02.1 · inverse_equivalence · neg_mul, add_inverse — An identity for all reals (checked as a polynomial identity on a grid in N1); two-way.
• S02 · inverse_equivalence · complex_mul_formula, complex_pair_eq — The formula is an equation and the pairs are equal because both components are; the step is two-way.
• S01 · premise_audit · G1, mko_modconj_def — This step only states the definitions and derives no new fact.

Error controls and negative controls

Conjugation changes only the sign of the imaginary part

One mistake the MKO names is changing the sign of the real part. The conjugate of 3−4i is 3+4i; writing −3−4i changes the wrong component, and −3+4i is −z, not z̄.

Distinguish the modulus squared from the modulus

Another mistake identified in the MKO is taking the modulus squared for the modulus. |3−4i|²=25 but |3−4i|=5; |1+2i|²=5 but |1+2i|=√5 is not an integer. Writing 2.236 is only an approximation: 2.236²=4.999696≠5 (N18). Following the MKO, this guide keeps the exact modulus squared.

The real part of z·z̄ is a²+b², not a²−b²

Using the difference of squares (a+bi)(a−bi)=a²−(bi)², the easiest slip is forgetting (bi)²=b²i²=−b², which gives the wrong a²−b²; for z=3−4i that is 9−16=−7. S02.1 shows that the plus sign comes from −b·(−b)=+b².

• The conjugate of 3−4i is −3−4i → reject — Conjugation changes only the sign of the imaginary coefficient: 3+4i.
• |3−4i|=25 → reject — 25 is the modulus squared; the modulus is √25=5.
• |1+2i|=2.236 exactly → reject — 2.236²=4.999696≠5; the exact modulus squared is 5 and the modulus is √5.
• (3−4i)(3+4i)=9−16=−7 → reject — i²=−1 makes the product 9+16=25, and z·z̄ is always nonnegative.

Result and limitations

For all reals a, b, c, d: z·z̄=(a²+b²)+0i is the real embedding of the modulus squared and is nonnegative; conjugation preserves addition and multiplication; |zw|²=|z|²|w|². For z=3−4i and w=1+2i: z̄=3+4i, |z|²=25, z·z̄=(25,0), |z|=5 (different from the modulus squared 25); w̄=1−2i, |w|²=5 (|w|=√5 is not an integer, so the exact modulus squared is kept); zw=11+2i, (zw)‾=11−2i=z̄·w̄, and |zw|²=125=25·5.

• Associativity and commutativity of multiplication in ℂ (used in S06.1) are prerequisites and are not derived here from the ordered-pair definition; complex division, arguments and polar form (the MKO's formal next) are not treated.
• N1 to N5 are polynomial-identity checks on grids, serving as cross-checks; the general results are proved by the algebra of S02 to S06.

Verification and source binding

19 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 4d35d95477cfaf8ae77bb1db462786967900da76e6b8489990bb52fed2f61c28
• original source SHA-256: 4d35d95477cfaf8ae77bb1db462786967900da76e6b8489990bb52fed2f61c28
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)