# Linear systems in two variables: the unique-solution formula, checking both rows, and consistency when D=0 [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-system-linear-equations/) 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-system-linear-equations-01 · production-20261019-adopted-96 ## Goal and scope (I) Solve 2x+3y=7, x−y=1: prove the unique-solution formula when D=ae−bd≠0, solve, and check by substituting into both rows; (II) decide x+2y=3, 2x+4y=7; (III) decide x+2y=3, 2x+4y=6; and use (IV) 0x+0y=1, 0x+0y=2 to show that D and both Cramer numerators being zero does not imply infinitely many solutions. Works inside the MKO's scope: two equations with real unknowns x, y; the four worked examples have integer coefficients, while the general unique-solution formula is proved for the real coefficients of G1. Proves completely that D≠0 gives exactly one solution with the stated formula; for D=0 decides each example by row operations (equivalences that preserve the solution set) as having no solution or infinitely many, checking zero rows. Does not prove a general rank criterion for D=0; does not guess solutions from sketched line intersections; does not change the canonical MKO or its English edition. ## Givens and symbols - eq_congruence - distributive - mul_inverse_nonzero - mul_zero - numeric_evaluation - solution_def - G1 — The unknowns x, y are real; the general system is ax+by=c, dx+ey=f with real coefficients and right sides; L(x,y)=(ax+by−c, dx+ey−f), z=(0,0) and D=ae−bd. - G2 — System I: 2x+3y=7, x−y=1, that is a=2, b=3, c=7, d=1, e=−1, f=1. - G3 — System II: x+2y=3, 2x+4y=7; System III: x+2y=3, 2x+4y=6; System IV: 0x+0y=1, 0x+0y=2 (zero-coefficient rows are allowed as constraints, MKO assumption a2). - ax+by=c,\ dx+ey=f — the two rows (real coefficients a to f) - L(x,y) — (ax+by−c, dx+ey−f) - z — the zero vector (0,0) - D — ae−bd, the 2×2 determinant - r_1,\ r_2 — the first and second row equations - r_2-\lambda r_1 — row two minus λ times row one ## Rules and sources - eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined. - mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d. - frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0. - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v). - mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw). - mul_one · prerequisite — Multiplicative identity: 1·u=u. - add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w). - add_zero · prerequisite — Additive identity: u+0=u. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B. - mko_linear_system · cited — For real unknowns x and y, require a x+b y=c and d x+e y=f simultaneously. Define L(x,y)=(a x+b y−c,d x+e y−f) and z=(0,0), so the solution set satisfies L(x,y)=z. If D=ae−bd≠0, the unique solution is x=(ce−bf)/D and y=(af−cd)/D. If D=0, check consistency: there may be no solution or infinitely many solutions. · mko-system-linear-equations - solution_def · prerequisite — (x,y)∈ℝ² is a solution of the system exactly when L(x,y)=z, that is, when both equations hold at once (equality of ordered pairs). - L_cramer · lemma — If D=ae−bd≠0, the system ax+by=c, dx+ey=f has exactly one solution, namely x=(ce−bf)/D, y=(af−cd)/D. - L_row_replace · lemma — For every real λ, the systems {ax+by=c, dx+ey=f} and {ax+by=c, (d−λa)x+(e−λb)y=f−λc} have the same solution set. ## Main derivation S01 · equivalentBefore L(x,y)=z After ax+by=c\ \land\ dx+ey=f Conditions: none Rule: solution_def · Uses: G1, solution_def, mko_linear_system Leaf basis: solution_def + cartesian_product_def + eq_congruence By the MKO, the solution set is described by L(x,y)=z. L(x,y)=(ax+by−c, dx+ey−f) equals z=(0,0) exactly when both components are 0, i.e. ax+by−c=0 and dx+ey−f=0, which after adding the constants to both sides says both equations hold at once. So 'solution' always means an (x,y) satisfying both rows. S02 · equivalentBefore D=ae-bd After D=2\cdot(-1)-3\cdot 1=-5\neq 0 Conditions: none Rule: numeric_evaluation · Uses: G2 Leaf basis: numeric_evaluation Substitute a=2, b=3, d=1, e=−1: D=2·(−1)−3·1=−2−3=−5, which is nonzero. S03 · theorem_applicationBefore D=-5\neq 0 After x=\frac{7\cdot(-1)-3\cdot 1}{-5}=2,\quad y=\frac{2\cdot 1-7\cdot 1}{-5}=1 Conditions: D\neq 0 Rule: L_cramer · Uses: S02, G2, L_cramer Leaf basis: eq_congruence + distributive + mul_inverse_nonzero + frac_rules Since D≠0, Lemma L_cramer applies: System I has exactly one solution, x=(ce−bf)/D=(−7−3)/(−5)=2 and y=(af−cd)/D=(2−7)/(−5)=1. So the unique solution is (2,1). The lemma is proved in sub-steps S03.1 to S03.4. S04 · impliesBefore (x,y)=(2,1) After 2\cdot 2+3\cdot 1=7\ \land\ 2-1=1 Conditions: none Rule: numeric_evaluation · Uses: S03, G2, solution_def Leaf basis: numeric_evaluation + solution_def Independent check: substitute (2,1) into both rows; row one gives 4+3=7 and row two gives 2−1=1, so both rows hold. This step does not depend on the formula and can catch arithmetic slips made in applying it. S05 · impliesBefore (x,y)=(5,-1) After 2\cdot 5+3\cdot(-1)=7,\ \ 5-(-1)=6\neq 1 Conditions: none Rule: solution_def · Uses: G2, solution_def Leaf basis: solution_def + numeric_evaluation The one-row trap: (5,−1) satisfies row one (10−3=7), but row two gives 5−(−1)=6≠1. By the definition of a solution both rows must hold at once, so (5,−1) is not a solution of System I. This agrees with the unique solution (2,1) of S03. S06 · impliesBefore x+2y=3,\ 2x+4y=7 After D=1\cdot 4-2\cdot 2=0 Conditions: none Rule: mko_linear_system · Uses: G3, mko_linear_system Leaf basis: mko_linear_system + numeric_evaluation System II has D=1·4−2·2=0, so L_cramer does not apply and the division in the formula is undefined. By the MKO, consistency must be checked separately when D=0. (Its Cramer numerator ce−bf=3·4−2·7=−2≠0, but this guide does not use numerators as the criterion; S07 decides directly by a row operation.) S07 · equivalentBefore x+2y=3\ \land\ 2x+4y=7 After x+2y=3\ \land\ 0x+0y=1 Conditions: \lambda=2 Rule: L_row_replace · Uses: S06, L_row_replace Leaf basis: eq_congruence + distributive + numeric_evaluation By Lemma L_row_replace with λ=2, replace row two by row two minus 2 times row one: (2−2·1)x+(4−2·2)y=7−2·3, that is 0x+0y=1. The new system has the same solution set as the original. S08 · impliesBefore 0x+0y=1 After 0=1\ \text{for every}\ (x,y),\ \text{solution set of II}=\varnothing Conditions: none Rule: mul_zero · Uses: S07, mul_zero, add_zero Leaf basis: mul_zero + add_zero + numeric_evaluation For every (x,y), 0x+0y=0+0=0 (multiplying by zero, additive identity), so 0x+0y=1 demands 0=1, which no (x,y) satisfies. By the equivalence in S07, System II has no solution. MKO assumption a2: a zero row 0=c with c≠0 is inconsistent. S09 · equivalentBefore x+2y=3\ \land\ 2x+4y=6 After x+2y=3\ \land\ 0x+0y=0\ \Leftrightarrow\ x+2y=3 Conditions: \lambda=2 Rule: L_row_replace · Uses: G3, L_row_replace, mul_zero, add_zero Leaf basis: eq_congruence + distributive + mul_zero + add_zero + and_intro_elim System III also has D=1·4−2·2=0. The same row operation with λ=2 turns row two into 0x+0y=6−2·3=0. For every (x,y), 0x+0y=0 always holds and imposes no restriction (MKO assumption a2), so System III is equivalent to the single equation x+2y=3. S10 · equivalentBefore \{(x,y)\in\mathbb{R}^2\mid x+2y=3\} After \{(3-2t,\,t)\mid t\in\mathbb{R}\} Conditions: none Rule: set_extensionality · Uses: S09, set_extensionality Leaf basis: set_extensionality + eq_congruence + add_inverse + numeric_evaluation ⊆: if x+2y=3, take t=y; then x=3−2t (subtract 2y from both sides), so (x,y)=(3−2t,t). ⊇: for every real t, (3−2t)+2t=3 (N17), so (3−2t,t) is a solution. Both directions hold, so the two sets are equal. S11 · impliesBefore \{(3-2t,\,t)\mid t\in\mathbb{R}\} After \text{infinitely many solutions, e.g.}\ (3,0),\ (1,1) Conditions: none Rule: cartesian_product_def · Uses: S10, cartesian_product_def Leaf basis: cartesian_product_def + injective_surjective_def + numeric_evaluation Different values of t give different solutions, because the second component is t itself (equal ordered pairs need equal second components). ℝ has infinitely many elements, so System III has infinitely many solutions. For example t=0 gives (3,0) and t=1 gives (1,1); both satisfy both original rows: 3+0=3, 6+0=6; 1+2=3, 2+4=6 (N18 checks row two for general t). S12 · impliesBefore 0x+0y=1,\ 0x+0y=2 After D=0,\ ce-bf=0,\ af-cd=0,\ \text{yet no solution} Conditions: none Rule: mul_zero · Uses: G3, mul_zero, add_zero Leaf basis: mul_zero + add_zero + numeric_evaluation System IV: a=b=d=e=0, c=1, f=2. D=0·0−0·0=0, ce−bf=1·0−0·2=0, af−cd=0·2−1·0=0, all three zero. Yet row one reads 0=1 for every (x,y), which is false, so the system has no solution. Hence 'D and both Cramer numerators are zero' does not imply infinitely many solutions; inconsistent zero rows must be checked first (MKO paragraph three). S13 · impliesBefore \text{S03, S04, S08, S10, S11, S12} After \text{I}:\ \{(2,1)\};\ \text{II}:\ \varnothing;\ \text{III}:\ \{(3-2t,t)\mid t\in\mathbb{R}\};\ \text{IV}:\ \varnothing Conditions: none Rule: and_intro_elim · Uses: S03, S04, S08, S10, S11, S12 Leaf basis: and_intro_elim Summary: System I has D=−5≠0 and the unique solution (2,1), checked in both rows; System II has D=0 and a row operation produces 0=1, so no solution; System III has D=0 and the row operation gives 0=0, with solution set {(3−2t,t) ∣ t∈ℝ}, infinitely many; System IV has all three determinant values zero yet no solution. ## Substeps and lemmas S03.1 · impliesBefore ax+by=c\ \land\ dx+ey=f After (ae-bd)x=ce-bf Conditions: none Rule: eq_congruence · Uses: eq_congruence, distributive Leaf basis: eq_congruence + distributive + mul_comm + add_inverse Let (x,y) be a solution. Multiply row one by e and row two by b, then subtract: e(ax+by)−b(dx+ey)=ec−bf. The left side expands to aex+bey−bdx−bey=(ae−bd)x (N4 checks this identity). So every solution satisfies (ae−bd)x=ce−bf. S03.2 · impliesBefore ax+by=c\ \land\ dx+ey=f After (ae-bd)y=af-cd Conditions: none Rule: eq_congruence · Uses: eq_congruence, distributive Leaf basis: eq_congruence + distributive + mul_comm + add_inverse Likewise eliminate x: multiply row two by a and row one by d, then subtract: a(dx+ey)−d(ax+by)=af−dc. The left side expands to adx+aey−adx−bdy=(ae−bd)y (N5). So every solution satisfies (ae−bd)y=af−cd. S03.3 · impliesBefore Dx=ce-bf,\quad Dy=af-cd,\quad D\neq 0 After x=\frac{ce-bf}{D},\quad y=\frac{af-cd}{D} Conditions: D\neq 0 Rule: mul_inverse_nonzero · Uses: S03.1, S03.2, mul_inverse_nonzero Leaf basis: mul_inverse_nonzero + eq_congruence + mul_assoc + mul_one Since D≠0, 1/D exists, and multiplying both equations by 1/D gives the values of x and y. So every solution equals this pair: there is at most one solution (uniqueness). If D=0 there is no 1/D and the step cannot be taken, which is exactly why the MKO forbids the unique-solution division when D=0. S03.4 · impliesBefore x_0=\frac{ce-bf}{D},\ y_0=\frac{af-cd}{D} After ax_0+by_0=c\ \land\ dx_0+ey_0=f Conditions: D\neq 0 Rule: frac_rules · Uses: frac_rules, distributive Leaf basis: frac_rules + distributive + mul_comm + add_inverse + mul_inverse_nonzero Existence: substituting into row one, ax₀+by₀=(a(ce−bf)+b(af−cd))/D=(ace−abf+abf−bcd)/D=c(ae−bd)/D=c; into row two, dx₀+ey₀=(d(ce−bf)+e(af−cd))/D=(cde−bdf+aef−cde)/D=f(ae−bd)/D=f (N6 and N7 check the two identities). S03.1 to S03.4 together prove Lemma L_cramer: when D≠0 there is exactly one solution. S07.1 · equivalentBefore ax+by=c\ \land\ dx+ey=f After ax+by=c\ \land\ (d-\lambda a)x+(e-\lambda b)y=f-\lambda c Conditions: none Rule: eq_congruence · Uses: eq_congruence, distributive Leaf basis: eq_congruence + distributive + add_inverse + add_assoc ⇒: assume both rows. Multiplying row one by λ gives λ(ax+by)=λc; subtracting this from both sides of row two gives (dx+ey)−λ(ax+by)=f−λc, which distributivity rearranges to (d−λa)x+(e−λb)y=f−λc; row one is kept. ⇐: assume the new system and add λ times row one back to the new row two, giving dx+ey=f. Both directions only apply the same operation to both sides of an equation. This proves Lemma L_row_replace. ## Reverse audits - S13 · sufficient_goal_reduction · S03, S04, S08, S10, S11, S12, and_intro_elim — Goal G: the verdicts on the four systems. Sufficient condition H: the conclusions of the listed steps; H⇒G is just conjunction, H is proved forwards from G1 to G3, and G is never used as a premise. - S12 · premise_audit · mul_zero, add_zero, numeric_evaluation — One concrete counterexample suffices to refute the general claim (N19 to N21); this step gives no general criterion for D=0. - S11 · premise_audit · S10, cartesian_product_def — It needs the parametrization to be injective (distinct t, distinct solutions); the examples only illustrate, and the conclusion comes from the parametrization. - S10 · inverse_equivalence · set_extensionality, eq_congruence — Both inclusions are proved, so the sets are equal. - S09 · inverse_equivalence · L_row_replace, mul_zero, add_zero, and_intro_elim — The row operation preserves the solution set both ways, and conjoining an always-true condition does not change truth, so it holds both ways. - S08 · premise_audit · mul_zero, add_zero, S07 — It needs the equivalence of solution sets from S07; D=0 alone does not imply no solution, an inconsistent zero row must actually appear. - S07.1 · inverse_equivalence · eq_congruence, distributive — Both directions have reasons; the key is that row one is kept, so its λ multiple can be added back. - S07 · inverse_equivalence · L_row_replace — Both directions of the lemma are proved in S07.1: subtracting 2 times row one and adding it back undo each other. - S06 · premise_audit · mko_linear_system, numeric_evaluation — D can be recomputed (N12, N22); this step only rules out the formula and does not yet decide the solution set. - S05 · premise_audit · solution_def, numeric_evaluation — Failure of one row is enough to exclude it (N10, N11). - S04 · premise_audit · solution_def, numeric_evaluation — Both rows must be checked (N8, N9); uniqueness comes from S03.3, not from this substitution. - S03.4 · premise_audit · frac_rules, distributive, mul_inverse_nonzero — Adding over the common denominator and cancelling D both need D≠0. Uniqueness (S03.3) together with existence (this step) gives 'exactly one solution'. - S03.3 · premise_audit · S03.1, S03.2, mul_inverse_nonzero — This step gives uniqueness only; that the pair really is a solution (existence) is proved separately in S03.4. - S03.2 · premise_audit · eq_congruence, distributive — As in S03.1, this is only a necessary condition; no converse is claimed. - S03.1 · premise_audit · eq_congruence, distributive — This is a necessary condition: it only derives an equation x must satisfy, and no converse is claimed (when D=0 this line may read 0=0 and restrict nothing). - S03 · premise_audit · S02, L_cramer — The only hypothesis is D≠0 (S02); the values are N2 and N3. The step is unavailable when D=0. - S02 · inverse_equivalence · numeric_evaluation — An exact integer computation, recomputable (N1). - S01 · inverse_equivalence · cartesian_product_def, eq_congruence — Equality of ordered pairs is two-way, and so is adding or subtracting a constant on both sides. ## Error controls and negative controls Checking one row is not enoughOne misconception named by the MKO is substituting into one row only. (5,−1) satisfies 2x+3y=7 yet gives x−y=6≠1 (S05). A candidate must be checked in both rows, and any denominators in it must first be confirmed nonzero. No division when D=0The second misconception identified in the MKO is dividing when D=0. Systems II and III both have D=0, yet one has no solution and the other infinitely many (S08, S11); dividing by 0 is undefined and could not tell these cases apart. They must be decided by solution-preserving row operations or a consistency check. Do not ignore a zero row 0=nonzeroThe third misconception identified in the MKO is ignoring an inconsistent zero row. 0x+0y=c with c≠0 fails for every (x,y), so the whole system has no solution (S08, S12). System IV has D and both Cramer numerators zero; looking only at these three numbers would wrongly suggest infinitely many solutions. - (5,−1) satisfies 2x+3y=7, so it is a solution of System I → reject — Row two gives 5−(−1)=6≠1; a solution must satisfy both rows. - The solution of System II is x=(3·4−2·7)/0 → reject — Division by 0 is undefined; a row operation turns System II into 0=1, so it has no solution. - System IV has D and both Cramer numerators zero, so it has infinitely many solutions → reject — Row one reads 0=1 for every (x,y), which is false, so there is no solution. - The only solution of System III is (3,0) → reject — (1,1) also satisfies both rows; the solution set is {(3−2t,t) ∣ t∈ℝ}, which is infinite. ## Result and limitations When D≠0 the system has exactly one solution x=(ce−bf)/D, y=(af−cd)/D (fully proved). System I (D=−5) has the unique solution (2,1), checked in both rows; (5,−1) satisfies only one row and is not a solution. System II (D=0) reduces to 0=1 and has no solution; System III (D=0) reduces to x+2y=3, with solution set {(3−2t,t) ∣ t∈ℝ}, infinitely many; System IV has D and both Cramer numerators zero, yet no solution. - The general rank and augmented-matrix consistency criterion for D=0 is not proved here; Systems II, III and IV are each decided by row operations or zero rows. - N4 to N7 are grid checks of polynomial identities (degree at most 2 in each variable) matching the expansions in S03.1 to S03.4; the argument does not depend on them. ## Verification and source binding 22 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 0f098bbbe0d8574f864b3569777f182c32f28dd1c5a192d61ca7d28c7748ec19 - original source SHA-256: 2f1efd35aa77f21aa1e0568cb94972c9eea89944a758fa7c0c901c5d58cc423a - 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-system-linear-equations-01.json)