# Complex modulus and conjugate: proving z·z̄=|z|² and that conjugation preserves the operations [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-complex-modulus-conjugate/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-complex-modulus-conjugate-01 · production-20261019-adopted-96 ## 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 uv holds; u0 give uwvw. - 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 S01 · definitionBefore z=a+bi\leftrightarrow(a,b) After \overline{z}=a-bi\leftrightarrow(a,-b),\ |z|^2=a^2+b^2 Conditions: none Rule: mko_modconj_def · Uses: G1, mko_modconj_def Leaf basis: mko_modconj_def + def_intro By the MKO, conjugation changes the sign of the imaginary coefficient only and leaves the real part alone: (a,b) becomes (a,−b); the modulus squared is the sum of squares of the components, a²+b². The modulus and its square are different notions: the modulus is the nonnegative square root of the modulus squared. S02 · equivalentBefore z\overline{z}=(a,b)\cdot(a,-b) After (a^2+b^2,\,0) Conditions: none Rule: complex_mul_formula · Uses: S01, complex_mul_formula Leaf basis: complex_mul_formula + complex_pair_eq Compute z·z̄ by the multiplication formula with c=a and d=−b: the real part is S02.1 and the imaginary coefficient is S02.2. S03 · impliesBefore z\overline{z}=(a^2+b^2,\,0) After z\overline{z}=|z|^2\in\mathbb{R},\ |z|^2\ge 0 Conditions: none Rule: real_embedding · Uses: S02, real_embedding, square_nonneg Leaf basis: real_embedding + square_nonneg + order_basics (a²+b²,0) is exactly the embedding of the real number a²+b²=|z|², so z·z̄ equals the real embedding of the modulus squared, as the MKO says. Also a²≥0 and b²≥0, so |z|²≥0, with equality only when a=b=0. S04 · equivalentBefore \overline{z+w}=\overline{(a+c)+(b+d)i} After (a+c)-(b+d)i=(a-bi)+(c-di)=\overline{z}+\overline{w} Conditions: none Rule: complex_addsub · Uses: G1, complex_addsub, S01 Leaf basis: complex_addsub + complex_pair_eq + distributive z+w has imaginary coefficient b+d, which conjugation turns into −(b+d)=−b−d; adding z̄+w̄ componentwise gives imaginary coefficient −b+(−d) as well. Both real parts are a+c, so conjugation preserves addition. S05 · equivalentBefore \overline{zw} After \overline{z}\cdot\overline{w} Conditions: none Rule: L_conj_mul · Uses: S01, complex_mul_formula Leaf basis: complex_mul_formula + complex_pair_eq + neg_mul Conjugation preserves multiplication (Lemma L_conj_mul). The proof is in S05.1 and S05.2: compute the ordered pair of each side and compare components. S06 · equivalentBefore |zw|^2 After |z|^2\,|w|^2 Conditions: none Rule: L_modsq_mul · Uses: S03, S05 Leaf basis: real_embedding + mul_assoc + mul_comm + complex_pair_eq From S03 and S05, the modulus squared is multiplicative (Lemma L_modsq_mul), proved in S06.1 and S06.2. N5 cross-checks independently with the polynomial identity (ac−bd)²+(ad+bc)²=(a²+b²)(c²+d²). S07 · equivalentBefore z=3-4i\leftrightarrow(3,-4) After \overline{z}=3+4i\leftrightarrow(3,4) Conditions: none Rule: mko_modconj_def · Uses: G2, S01 Leaf basis: mko_modconj_def Only the imaginary coefficient −4 changes sign to 4; the real part 3 is unchanged. Writing −3−4i or −3+4i is wrong (the first changes the real part, the second is −z). S08 · impliesBefore |z|^2=3^2+(-4)^2,\ z\overline{z}=(3,-4)(3,4) After |z|^2=25,\ z\overline{z}=(3\cdot3-(-4)\cdot4,\,3\cdot4+(-4)\cdot3)=(25,0) Conditions: none Rule: complex_mul_formula · Uses: S07, S02, complex_mul_formula Leaf basis: complex_mul_formula + numeric_evaluation The modulus squared is 9+16=25. Computing z·z̄ directly by the formula: real part 9+16=25, imaginary coefficient 12−12=0, giving (25,0), the real embedding of 25, in line with the general results S02 and S03. S09 · impliesBefore |z|^2=25 After |z|=\sqrt{25}=5\neq 25 Conditions: 5\ge 0 Rule: sqrt_def · Uses: S08, modulus_def, sqrt_def Leaf basis: sqrt_def + modulus_def + numeric_evaluation The modulus is the nonnegative square root of the modulus squared. Since 5≥0 and 5²=25, uniqueness of the square root gives |z|=5. The modulus squared 25 and the modulus 5 are different numbers, which is the mistake the MKO names. S10 · impliesBefore w=1+2i After \overline{w}=1-2i,\ |w|^2=5,\ |w|=\sqrt5\notin\mathbb{Z} Conditions: none Rule: mko_modconj_def · Uses: G2, G3, S01 Leaf basis: mko_modconj_def + order_basics + case_analysis + numeric_evaluation w̄=(1,−2) and |w|²=1+4=5. 5 is not a perfect square: a nonnegative integer n≤2 has n²≤4 and n≥3 has n²≥9, so no integer squares to 5. Hence |w|=√5 is not an integer; by G3 the exact modulus squared 5 is kept and no decimal such as 2.236 is written. S11 · equivalentBefore zw=(3,-4)(1,2) After (3\cdot1-(-4)\cdot2,\,3\cdot2+(-4)\cdot1)=(11,2) Conditions: none Rule: complex_mul_formula · Uses: G2, complex_mul_formula Leaf basis: complex_mul_formula + numeric_evaluation Real part 3+8=11, imaginary coefficient 6−4=2, so zw=11+2i. S12 · impliesBefore \overline{zw}\ \text{vs}\ \overline{z}\,\overline{w}=(3,4)(1,-2) After (11,-2)=(3\cdot1-4\cdot(-2),\,3\cdot(-2)+4\cdot1) Conditions: none Rule: complex_mul_formula · Uses: S11, S07, S10, S05 Leaf basis: complex_mul_formula + complex_pair_eq + numeric_evaluation Left: (zw)‾=(11,−2). Right: z̄·w̄=(3,4)(1,−2), real part 3+8=11, imaginary coefficient −6+4=−2. The two sides agree, an instance of S05. S13 · impliesBefore |zw|^2=11^2+2^2 After 125=25\cdot5=|z|^2|w|^2 Conditions: none Rule: L_modsq_mul · Uses: S11, S08, S10, S06 Leaf basis: L_modsq_mul + numeric_evaluation 121+4=125 and |z|²|w|²=25·5=125 agree, an instance of S06. Even though |w| is not an integer, the modulus squares stay exact integers. S14 · impliesBefore \overline{z+w}=\overline{(4,-2)} After (4,2)=(3,4)+(1,-2)=\overline{z}+\overline{w} Conditions: none Rule: complex_addsub · Uses: G2, S04, S07, S10 Leaf basis: complex_addsub + numeric_evaluation z+w=(3+1, −4+2)=(4,−2), whose conjugate is (4,2); z̄+w̄=(3+1, 4−2)=(4,2). The sides agree, an instance of S04. S15 · impliesBefore z=a+bi,\ w=c+di After 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 Conditions: none Rule: and_intro_elim · Uses: S03, S04, S05, S06 Leaf basis: and_intro_elim + forall_intro Combine the four general results; they hold for all real components, and the integer examples of S07 to S14 are only checks. ## Substeps and lemmas S02.1 · equivalentBefore \operatorname{Re}(z\overline{z})=a\cdot a-b\cdot(-b) After a^2+b^2 Conditions: none Rule: neg_mul · Uses: complex_mul_formula, neg_mul Leaf basis: neg_mul + add_inverse + power_laws In the real part ac−bd put c=a and d=−b: a·a−b·(−b). Since b·(−b)=−b², subtracting −b² adds b², giving a²+b². The plus sign comes from the product of i²=−1 with the conjugate's minus sign. S02.2 · equivalentBefore \operatorname{Im}(z\overline{z})=a\cdot(-b)+b\cdot a After 0 Conditions: none Rule: mul_comm · Uses: complex_mul_formula, mul_comm Leaf basis: mul_comm + neg_mul + add_inverse In the imaginary coefficient ad+bc put d=−b and c=a: a·(−b)+b·a=−ab+ab=0 (commutativity gives ba=ab). So z·z̄ has zero imaginary part and is real. S05.1 · equivalentBefore \overline{zw}=\overline{(ac-bd)+(ad+bc)i} After (ac-bd,\,-(ad+bc)) Conditions: none Rule: complex_mul_formula · Uses: complex_mul_formula, S01 Leaf basis: complex_mul_formula + mko_modconj_def First write zw=(ac−bd)+(ad+bc)i by the multiplication formula, then conjugate: the real part stays and the imaginary coefficient changes sign. S05.2 · equivalentBefore \overline{z}\cdot\overline{w}=(a,-b)\cdot(c,-d) After (ac-(-b)(-d),\,a(-d)+(-b)c)=(ac-bd,\,-(ad+bc)) Conditions: none Rule: neg_mul · Uses: S05.1, complex_mul_formula, neg_mul Leaf basis: neg_mul + distributive + complex_pair_eq Apply the multiplication formula to (a,−b) and (c,−d): real part ac−(−b)(−d)=ac−bd (two minus signs give a plus); imaginary coefficient a(−d)+(−b)c=−ad−bc=−(ad+bc). Both components match S05.1, so by equality of ordered pairs (zw)‾=z̄·w̄. S05.1 and S05.2 together prove Lemma L_conj_mul. S06.1 · equivalentBefore (|zw|^2,0)=(zw)\,\overline{zw} After (zw)(\overline{z}\,\overline{w})=(z\overline{z})(w\overline{w}) Conditions: none Rule: mul_assoc · Uses: S03, S05, mul_assoc, mul_comm Leaf basis: eq_replace + mul_assoc + mul_comm Apply S03 to the complex number zw: (zw)·(zw)‾ is the embedding of |zw|². Replace (zw)‾ by z̄·w̄ using S05, then regroup the four factors as (z z̄)(w w̄) by associativity and commutativity of multiplication in ℂ. S06.2 · impliesBefore (z\overline{z})(w\overline{w})=(|z|^2,0)(|w|^2,0) After (|z|^2|w|^2,\,0)\ \Rightarrow\ |zw|^2=|z|^2|w|^2 Conditions: none Rule: real_embedding · Uses: S06.1, S03, real_embedding, complex_pair_eq Leaf basis: real_embedding + complex_pair_eq By S03, z z̄ and w w̄ are the embeddings of |z|² and |w|²; the product of two embedded reals is (|z|²|w|²,0). Comparing real parts gives |zw|²=|z|²|w|². S06.1 and S06.2 together prove Lemma L_modsq_mul. ## 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 partOne 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 modulusAnother 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-complex-modulus-conjugate-01.json)