# Complex numbers: computing (2+3i)(4−5i) as an ordered pair and deciding equality [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-complex-number/) 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-number-01 · production-20261019-adopted-96 ## Goal and scope Let z=2+3i and w=4−5i. Find z+w, z−w and z·w as ordered pairs (real part, imaginary coefficient). For the product, first derive the general formula (a+bi)(c+di)=(ac−bd)+(ad+bc)i from distributivity and i²=−1, then substitute the numbers and cross-check by direct expansion; finally decide whether z·w equals the real number 23. Works inside the MKO's scope: integer real parts and imaginary coefficients (regarded as real numbers), the three operations addition, subtraction and multiplication, and answers as ordered pairs; no complex division, conjugate, modulus or polar form. The commutative, associative and distributive laws of addition and multiplication in ℂ are used as prerequisites and are not derived here from the ordered-pair construction. The canonical MKO and its English edition are not changed. ## Givens and symbols - distributive - mul_assoc - mul_comm - add_comm - add_assoc - numeric_evaluation - G1 — z=2+3i and w=4−5i; the real parts and imaginary coefficients are integers. - G2 — Answers are ordered pairs (real part, imaginary coefficient); the order of the components is semantic data and no value is read off a picture or an unmarked scale; complex division is not used (MKO assumptions a1, a2). - z=a+bi — the complex number with real part a and imaginary coefficient b - (a,b) — the ordered pair of z, in the order (real part, imaginary coefficient) - i — the imaginary unit, with i^2=-1 - z,\ w — the two given complex numbers ## Rules and sources - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw). - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - add_comm · prerequisite — Commutativity of addition: u+v=v+u. - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv. - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - mko_complex_def · cited — A complex number z=a+b*i is uniquely determined by its real part a and imaginary coefficient b and can be viewed as the ordered pair (a,b) in the complex plane. Addition and subtraction are componentwise; multiplication follows from distributivity and i²=−1. · mko-complex-number - complex_pair_eq · prerequisite — For reals a, b, c, d: a+bi=c+di if and only if a=c and b=d; hence a+bi corresponds one-to-one to the ordered pair (a,b). - complex_addsub · prerequisite — Componentwise addition and subtraction: (a+bi)+(c+di)=(a+c)+(b+d)i and (a+bi)−(c+di)=(a−c)+(b−d)i. - i_squared · prerequisite — The imaginary unit satisfies i²=i·i=−1. - real_embedding · prerequisite — A real number r is embedded as the complex number r+0i, the ordered pair (r,0). - L_complex_mul · lemma — For all reals a, b, c, d: (a+bi)(c+di)=(ac−bd)+(ad+bc)i; in ordered pairs, (a,b)·(c,d)=(ac−bd, ad+bc). ## Main derivation S01 · definitionBefore z=2+3i,\ w=4-5i After z\leftrightarrow(2,3),\ w\leftrightarrow(4,-5) Conditions: none Rule: mko_complex_def · Uses: G1, G2 Leaf basis: mko_complex_def + complex_pair_eq By the MKO, a complex number a+bi is determined by its real part a and imaginary coefficient b and corresponds to the ordered pair (a,b). z has real part 2 and imaginary coefficient 3; w=4−5i=4+(−5)i has imaginary coefficient −5: the minus sign belongs to the coefficient and must not be dropped. S02 · equivalentBefore z+w After (2+4)+(3+(-5))i=6-2i\leftrightarrow(6,-2) Conditions: none Rule: complex_addsub · Uses: S01, complex_addsub Leaf basis: complex_addsub + numeric_evaluation Addition is componentwise: real part 2+4=6, imaginary coefficient 3+(−5)=−2, so z+w=6−2i, the ordered pair (6,−2). S03 · equivalentBefore z-w After (2-4)+(3-(-5))i=-2+8i\leftrightarrow(-2,8) Conditions: none Rule: complex_addsub · Uses: S01, complex_addsub Leaf basis: complex_addsub + add_inverse + numeric_evaluation Subtraction is also componentwise: real part 2−4=−2, imaginary coefficient 3−(−5)=3+5=8. Subtracting a negative number adds its opposite; this is where signs are most easily lost. S04 · equivalentBefore (a+bi)(c+di) After (ac-bd)+(ad+bc)i Conditions: a,b,c,d\in\mathbb{R} Rule: L_complex_mul · Uses: mko_complex_def, i_squared Leaf basis: distributive + mul_assoc + mul_comm + i_squared + add_comm The MKO says multiplication follows from distributivity and i²=−1; it is not componentwise. First prove the general formula for arbitrary reals a, b, c, d (Lemma L_complex_mul) in sub-steps S04.1 to S04.3; the products below are then computed with it. S05 · theorem_applicationBefore zw=(2+3i)(4+(-5)i) After zw=(2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i Conditions: a=2,\ b=3,\ c=4,\ d=-5 Rule: L_complex_mul · Uses: S01, S04 Leaf basis: L_complex_mul + forall_elim Substitute a=2, b=3, c=4, d=−5 into the lemma. d must be −5, not 5: the imaginary coefficient of w is substituted together with its sign. S06 · equivalentBefore (2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i After 23+2i Conditions: none Rule: numeric_evaluation · Uses: S05 Leaf basis: numeric_evaluation Real part: 8−(−15)=8+15=23; imaginary coefficient: −10+12=2. So zw=23+2i. S07 · equivalentBefore (2+3i)(4-5i) After 8-10i+12i-15i^2=8+2i+15=23+2i Conditions: none Rule: i_squared · Uses: S01, distributive, i_squared Leaf basis: distributive + mul_assoc + mul_comm + i_squared + numeric_evaluation Cross-check by direct expansion without the formula: distributivity gives 2·4+2·(−5i)+3i·4+3i·(−5i)=8−10i+12i−15i²; i²=−1 turns −15i² into +15; collecting gives 23+2i, the same as S06. S08 · equivalentBefore zw=23+2i After zw\leftrightarrow(23,2) Conditions: none Rule: complex_pair_eq · Uses: S06, complex_pair_eq Leaf basis: complex_pair_eq By G2 the answer is written as the ordered pair (real part, imaginary coefficient)=(23,2). The order is semantic data: (2,23) stands for 2+23i, a different complex number. S09 · impliesBefore (23,2)\ \text{vs}\ (2,23) After (23,2)\neq(2,23) Conditions: none Rule: complex_pair_eq · Uses: S08, complex_pair_eq Leaf basis: complex_pair_eq + numeric_evaluation Two ordered pairs are equal only if the real parts agree and the imaginary coefficients agree; 23≠2, so (23,2)≠(2,23). Swapping the real and imaginary parts gives a different complex number, which is the common mistake the MKO names. S10 · definitionBefore 23\in\mathbb{R} After 23=23+0i\leftrightarrow(23,0) Conditions: none Rule: real_embedding · Uses: real_embedding Leaf basis: real_embedding To decide whether zw equals the real number 23, first embed 23 in the complex numbers: 23=23+0i, the ordered pair (23,0). The comparison must take place in one set, ℂ. S11 · equivalentBefore zw=23 After 23=23\ \land\ 2=0 Conditions: none Rule: complex_pair_eq · Uses: S08, S10, complex_pair_eq Leaf basis: complex_pair_eq + and_intro_elim zw=23 is equivalent to (23,2)=(23,0), which in turn is equivalent to both components agreeing: 23=23 and 2=0. S12 · impliesBefore 23=23\ \land\ 2=0 After zw\neq 23 Conditions: none Rule: contradiction · Uses: S11 Leaf basis: contradiction + and_intro_elim + numeric_evaluation 2=0 is false, so the conjunction is false, and by the equivalence S11, zw=23 fails. This is the MKO's third paragraph: a complex number with nonzero imaginary coefficient equals no real number, whatever its real part. S13 · theorem_applicationBefore wz=(4+(-5)i)(2+3i) After wz=(4\cdot 2-(-5)\cdot 3)+(4\cdot 3+(-5)\cdot 2)i=23+2i Conditions: a=4,\ b=-5,\ c=2,\ d=3 Rule: L_complex_mul · Uses: S04, G1 Leaf basis: L_complex_mul + numeric_evaluation Compute wz in the other order as a further check: the lemma gives real part 8+15=23 and imaginary coefficient 12−10=2, the same as zw, consistent with commutativity of multiplication in ℂ. S14 · impliesBefore z=2+3i,\ w=4-5i After z+w\leftrightarrow(6,-2),\ z-w\leftrightarrow(-2,8),\ zw\leftrightarrow(23,2),\ zw\neq 23 Conditions: none Rule: and_intro_elim · Uses: S02, S03, S08, S12 Leaf basis: and_intro_elim Combine the four conclusions: sum (6,−2), difference (−2,8), product (23,2), and the product is not the real number 23. ## Substeps and lemmas S04.1 · equivalentBefore (a+bi)(c+di) After ac+a(di)+(bi)c+(bi)(di) Conditions: none Rule: distributive · Uses: distributive, mul_comm Leaf basis: distributive + mul_comm Distribute over the second factor: (a+bi)(c+di)=(a+bi)c+(a+bi)(di); then distribute once more in each term (right distribution is turned into left distribution by commutativity), giving the four terms ac, a(di), (bi)c and (bi)(di). S04.2 · equivalentBefore ac+a(di)+(bi)c+(bi)(di) After ac+(ad)i+(bc)i+(bd)i^2 Conditions: none Rule: mul_assoc · Uses: S04.1, mul_assoc, mul_comm Leaf basis: mul_assoc + mul_comm Regroup and reorder the factors of each term by associativity and commutativity of multiplication: a(di)=(ad)i, (bi)c=(bc)i and (bi)(di)=(bd)(i·i)=(bd)i². Only the grouping and order of the factors change, not the value. S04.3 · equivalentBefore ac+(ad)i+(bc)i+(bd)i^2 After (ac-bd)+(ad+bc)i Conditions: none Rule: i_squared · Uses: S04.2, i_squared, distributive Leaf basis: i_squared + neg_mul + add_comm + add_assoc + distributive Substitute i²=−1: (bd)i²=(bd)(−1)=−bd, a term without i, so it belongs to the real part. Then commutativity and associativity of addition put the real terms ac and −bd together, and distributivity combines (ad)i+(bc)i into (ad+bc)i. S04.1 to S04.3 together prove Lemma L_complex_mul; the minus sign in −bd comes exactly from i²=−1. ## Reverse audits - S14 · sufficient_goal_reduction · S02, S03, S08, S12, and_intro_elim — Goal G: the three results and the equality decision. Sufficient condition H: the four proved conclusions S02, S03, S08 and S12; H⇒G by conjunction introduction. H is derived forwards from the givens; G is never used as a premise. - S13 · premise_audit · L_complex_mul, mul_comm, numeric_evaluation — This is a consistency check for one pair of numbers and does not prove commutativity, which is a prerequisite of this guide. - S12 · premise_audit · S11, contradiction, numeric_evaluation — Only one component, 2≠0, is used; equal real parts (23=23) are not enough for equality. - S11 · inverse_equivalence · complex_pair_eq — The equality condition for ordered pairs is itself two-way, so the step holds in both directions. - S10 · premise_audit · real_embedding — This step only writes out the embedding and derives no new fact. - S09 · premise_audit · complex_pair_eq, numeric_evaluation — One differing component suffices for inequality; the converse (inequality forces a particular component to differ) is not claimed. - S08 · inverse_equivalence · complex_pair_eq, G2 — a+bi and (a,b) correspond one-to-one, so writing the pair and writing back 23+2i are inverse moves. - S07 · inverse_equivalence · distributive, i_squared, numeric_evaluation — Every equals sign is a rewriting by equals; two independent routes give the same result, which catches copying and sign errors. - S06 · inverse_equivalence · numeric_evaluation — Exact evaluation of integer expressions, independently recomputable (N5, N6); both sides are the same number, so the step is two-way. - S05 · premise_audit · S01, L_complex_mul, forall_elim — The lemma holds for all real numbers, including the integers 2, 3, 4, −5, so they may be substituted; the step does not claim that the factors can be recovered from the product. - S04.3 · inverse_equivalence · i_squared, distributive, add_comm, add_assoc — Each move replaces an expression by an equal one (i² by −1, reordering and combining terms); undoing them in order restores the original, so the step is two-way. - S04.2 · inverse_equivalence · mul_assoc, mul_comm — Associativity and commutativity are identities for all complex numbers; reordering backwards returns the original expression. - S04.1 · inverse_equivalence · distributive, mul_comm — Backward, the four terms are recombined into the product of the two factors by distributivity; distributivity is an equation, so both directions hold. - S04 · inverse_equivalence · L_complex_mul — Both sides are two ways of writing the same complex number; every sub-step is a rewriting by equals, so the identity holds in both directions. - S03 · inverse_equivalence · complex_addsub, numeric_evaluation — Backward: (−2+8i)+w=(−2+4)+(8+(−5))i=2+3i=z, which restores z−w=−2+8i. - S02 · inverse_equivalence · complex_addsub, numeric_evaluation — Backward: (6−2i)−w=(6−4)+(−2−(−5))i=2+3i=z, which restores z+w=6−2i; both expressions name the same complex number. - S01 · premise_audit · G1, G2, mko_complex_def, complex_pair_eq — This step only rewrites the givens as ordered pairs and derives no new fact; the correspondence is one-to-one (complex_pair_eq), so computing with ordered pairs loses no information. ## Error controls and negative controls Forgetting i²=−1One mistake the MKO names is forgetting i²=−1 in multiplication. Treating −15i² as −15 (that is, taking i² as 1) gives (8−15)+2i=−7+2i; dropping the i² term gives 8+2i. Correctly, −15i²=−15·(−1)=+15 and the real part is 23. S04.3 shows that the −bd in the general formula is exactly this sign. Swapping the real and imaginary partsAnother mistake identified in the MKO is swapping the real and imaginary parts. The answer (23,2) means 23+2i; writing (2,23) gives 2+23i, a different number (S09). The order of the pair is semantic data and is not guessed from positions in a picture. Multiplication is not componentwiseAddition and subtraction are componentwise, but multiplication is not: (2,3)·(4,−5) is not (2·4, 3·(−5))=(8,−15). In the correct formula the real part ac−bd mixes both real parts and both imaginary coefficients, and the imaginary coefficient ad+bc is the sum of the cross terms. - (2+3i)(4−5i)=8−15i, because multiplication is componentwise → reject — Multiplication follows from distributivity and i²=−1; the correct product is 23+2i. - (2+3i)(4−5i)=−7+2i → reject — This takes i² as +1; in fact −15i²=+15 and the real part is 8+15=23. - The ordered pair of zw is (2,23) → reject — The order is (real part, imaginary coefficient); zw=23+2i corresponds to (23,2), and (2,23)≠(23,2). - 23+2i has real part 23, so it equals the real number 23 → reject — 23 embeds as (23,0), and equality would also need 2=0, which fails. ## Result and limitations z+w=6−2i, that is (6,−2); z−w=−2+8i, that is (−2,8); z·w=23+2i, that is (23,2), obtained both from the general formula (a+bi)(c+di)=(ac−bd)+(ad+bc)i and by direct expansion. Since the imaginary coefficient 2≠0, z·w is not the real number 23. - The commutative, associative and distributive laws in ℂ are prerequisites of this guide and are not derived from the ordered-pair definition; complex division, conjugates, moduli and polar form (the MKO's formal next) are not treated. - N13, recomputing i·i=−1 with the lemma, is only a consistency check; the lemma itself uses i²=−1, so it is not a proof of i²=−1. ## Verification and source binding 13 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 311fc9976ea86edccc67e94b6680145f12b64abe38568601a6bbabf8fd324b42 - original source SHA-256: 311fc9976ea86edccc67e94b6680145f12b64abe38568601a6bbabf8fd324b42 - 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-number-01.json)