Complex numbers: computing (2+3i)(4−5i) as an ordered pair and deciding equality

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

z=2+3i,\ w=4-5i

z\leftrightarrow(2,3),\ w\leftrightarrow(4,-5)

z+w

(2+4)+(3+(-5))i=6-2i\leftrightarrow(6,-2)

z-w

(2-4)+(3-(-5))i=-2+8i\leftrightarrow(-2,8)

(a+bi)(c+di)

(ac-bd)+(ad+bc)i

zw=(2+3i)(4+(-5)i)

zw=(2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i

(2\cdot 4-3\cdot(-5))+(2\cdot(-5)+3\cdot 4)i

23+2i

(2+3i)(4-5i)

8-10i+12i-15i^2=8+2i+15=23+2i

zw=23+2i

zw\leftrightarrow(23,2)

(23,2)\ \text{vs}\ (2,23)

(23,2)\neq(2,23)

23\in\mathbb{R}

23=23+0i\leftrightarrow(23,0)

zw=23

23=23\ \land\ 2=0

23=23\ \land\ 2=0

zw\neq 23

wz=(4+(-5)i)(2+3i)

wz=(4\cdot 2-(-5)\cdot 3)+(4\cdot 3+(-5)\cdot 2)i=23+2i

z=2+3i,\ w=4-5i

z+w\leftrightarrow(6,-2),\ z-w\leftrightarrow(-2,8),\ zw\leftrightarrow(23,2),\ zw\neq 23

Substeps and lemmas

(a+bi)(c+di)

ac+a(di)+(bi)c+(bi)(di)

ac+a(di)+(bi)c+(bi)(di)

ac+(ad)i+(bc)i+(bd)i^2

ac+(ad)i+(bc)i+(bd)i^2

(ac-bd)+(ad+bc)i

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²=−1

One 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 parts

Another 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 componentwise

Addition 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)