Equation: solving x²/(x−1)=1/(x−1) inside its domain

Goal and scope

With allowed domain ℝ, find the solution set of the equation x²/(x−1)=1/(x−1), and explain why the equation x²=1 obtained by multiplying both sides by x−1 has two solutions while the original has only one.

Follows the MKO's definition: the solution set consists of the allowed x at which both sides are defined and equal. Treats one real equation with fractions, illustrating the domain, equivalence under multiplication by a nonzero expression, the zero-product property, rejecting a candidate and checking by substitution. It does not treat the general theory of rational equations or complex solutions, and does not change the canonical MKO or its English edition.

Givens and symbols

• mul_inverse_nonzero
• eq_congruence
• distributive
• zero_product
• set_builder
• numeric_evaluation

• G1 — Allowed domain and operations: the variable x ranges over ℝ; real addition, subtraction, multiplication and division are used, and v/u is defined only when u≠0 (mul_inverse_nonzero).
• G2 — The equation: L(x)=R(x), where L(x)=x²/(x−1) and R(x)=1/(x−1).
• G3 — Definition of the solution set (MKO): 𝒮={x∈ℝ ∣ L(x) and R(x) are both defined and L(x)=R(x)}.

• L(x)=\frac{x^2}{x-1} — the left-hand expression
• R(x)=\frac{1}{x-1} — the right-hand expression
• D — the set of x at which both sides are defined
• \mathcal{S} — the solution set of the original equation
• u\neq 0 — the nonzero condition needed to divide by u or to use 1/u

Rules and sources

• 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.
• 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.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• 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.
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• 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.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_equation · cited — Given two expressions L(x) and R(x) in a common context, the solution set of L(x)=R(x) consists of all allowed x for which both sides are defined and equal. · mko-equation
• L_zero_diff · lemma — For reals u and c: u−c=0 ⇔ u=c.
• L_den · lemma — For reals a, b and u≠0: a/u=b/u ⇔ a=b.

Main derivation

L(x)=R(x)\ \text{over}\ \mathbb{R}

\mathcal{S}=\{x\in\mathbb{R}\mid L(x),R(x)\ \text{defined}\ \land\ L(x)=R(x)\}

L(x)\ \text{and}\ R(x)\ \text{defined}

x-1\neq 0

x-1\neq 0

x\neq 1;\quad D=\{x\in\mathbb{R}\mid x\neq 1\}

\frac{x^2}{x-1}=\frac{1}{x-1},\ x\in D

x^2=1,\ x\in D

x^2=1

x^2-1=0

x^2-1=0

(x-1)(x+1)=0

(x-1)(x+1)=0

x-1=0\ \lor\ x+1=0

x-1=0\ \lor\ x+1=0

x=1\ \lor\ x=-1

x\in D:\ L(x)=R(x)

\mathcal{S}=\{x\in\mathbb{R}\mid x\in D\ \land\ (x=1\lor x=-1)\}

x=1

1\notin D,\ \text{so}\ 1\notin\mathcal{S}

x=-1

-1\in D,\ \text{so}\ -1\in\mathcal{S}

x\in\mathcal{S}\iff x\in D\land(x=1\lor x=-1)

\mathcal{S}=\{-1\}

x=-1\ \text{in}\ L,\ R

L(-1)=\frac{1}{-2}=-\tfrac{1}{2}=R(-1)

\{x\in\mathbb{R}\mid x^2=1\}

\{-1,1\}\supsetneq\mathcal{S}=\{-1\}

\mathcal{S}=\{-1\},\ \{x\mid x^2=1\}=\{-1,1\}

\text{answer: }\mathcal{S}=\{-1\};\ 1\ \text{excluded since}\ 1\notin D

Substeps and lemmas

u-c=0

(u-c)+c=0+c

(u-c)+c=0+c

u=c

\frac{a}{u}=\frac{b}{u}

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

a=b

Reverse audits

• S15 · sufficient_goal_reduction · S12, S13, S14, and_intro_elim — Goal G: find 𝒮 and explain the extra solution of x²=1. Sufficient condition H: S12 (𝒮={−1}) and S14 (the extra solution comes from x−1=0); H⇒G is immediate. H is proved forwards from G1 to G3 without using G as a premise; S13 is an independent check.
• S14 · premise_audit · S05, S08, S12, set_extensionality — The two sets differ only by 1, and 1∉D; this explains the difference here, without claiming anything general about every possible multiplier.
• S13 · premise_audit · S12, G2, numeric_evaluation — This is an independent check of x=−1; it confirms that −1 is a solution but cannot by itself show there are no others, which is the job of the chain of equivalences S04 to S12.
• S12 · premise_audit · S10, S11, set_extensionality, case_analysis — Both inclusions are needed: 𝒮⊆{−1} uses S10 to exclude x=1, and {−1}⊆𝒮 uses S11.
• S11 · premise_audit · S03, S09, set_builder — Both conjuncts were checked: x∈D and x=1∨x=−1.
• S10 · premise_audit · S03, S09, set_builder — It is enough that 1 fails the conjunct x∈D; the two sides need not (and cannot) be computed.
• S09 · inverse_equivalence · logic_chain, S04, S08 — Every link is two-way, and S04 is used only for x∈D; so the chained equivalence holds only in D, and x∈D is kept as part of the set condition.
• S08 · inverse_equivalence · L_zero_diff, numeric_evaluation — Substituting back: 1−1=0 and (−1)+1=0; both branches are two-way equivalences.
• S07 · inverse_equivalence · zero_product — Forwards needs that ℝ has no zero divisors; backwards uses u·0=0. Both directions are contained in zero_product.
• S06 · inverse_equivalence · distributive, eq_replace — This is an identity for all reals (N4 is an independent polynomial check), and the replacement of equals is two-way.
• S05 · inverse_equivalence · L_zero_diff — Both directions of the lemma are proved; this step holds for every real and does not depend on x∈D.
• S04.2 · inverse_equivalence · mul_assoc, mul_comm, mul_inverse_nonzero, mul_one — The replacement of equals holds both ways; (1/u)u=1 needs u≠0.
• S04.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, mul_assoc — Backward multiplication by 1/u requires u≠0. If u=0, a/u and b/u are already undefined; they cannot be multiplied by zero and then evaluated as zero. Separately, multiplying two defined real expressions by zero loses their original information. That warning is not an evaluation of this step at u=0.
• S04 · inverse_equivalence · L_den, S03 — The backward move multiplies both sides by 1/(x−1) and needs x−1≠0; outside D (at x=1) it cannot be made, which is why 'x∈D' is carried along here.
• S03.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — Expressions are only replaced by equal ones, so whether the equation holds is unchanged and the step is two-way.
• S03.1 · inverse_equivalence · eq_congruence, add_inverse — Adding c and adding −c undo each other and can be done for every real, with no side condition.
• S03 · inverse_equivalence · L_zero_diff — Negating both sides of an equivalence gives an equivalence; both directions of the lemma are proved in the sub-steps.
• S02 · inverse_equivalence · mul_inverse_nonzero — If x−1≠0 then 1/(x−1) exists and both sides are defined; if x−1=0 both sides contain a division by 0 and neither is defined. Both directions have reasons.
• S01 · premise_audit · G1, G2, G3, mko_equation — This step only writes out the definition of the solution set and derives no new fact.

Error controls and negative controls

Multiplying by an expression that may be zero

The MKO lists the mistakes of claiming the solution set is unchanged after multiplying by zero and of dividing by an expression that may be zero. Multiplying both sides by x−1 is an equivalence only where x−1≠0 (S04); at x=1 the multiplier is 0, the step cannot be reversed, and x²=1 gains the solution 1 (S14). The correct procedure is to write the domain D={x ∣ x≠1} first and keep x∈D throughout the chain of equivalences.

Substitute candidates into the original equation

The MKO warns that candidates must be substituted back into the original equation. Substituting 1 makes both sides a division by 0, undefined, so 1 is not a solution (S10); substituting −1 makes both sides −1/2 (S13). Checking only in x²=1 would wrongly accept 1, because x²=1 is no longer the original equation.

Cancelling does not remove the domain

For the similar equation (x²−1)/(x−1)=2, cancelling first to x+1=2 gives x=1; but at x=1 the left side divides by 0 and is undefined. The cancellation (x²−1)/(x−1)=x+1 holds only for x≠1, so this equation's solution set is empty. Simplifying one side must carry along the condition under which the simplification holds.

• The solution set of the original equation is {−1,1} → reject — At x=1, 1−1=0 and neither side is defined, so 1∉𝒮 (S10).
• x=1 is a solution because 1²=1 → reject — That checks x²=1, not the original equation; the original has both sides undefined at x=1.
• Multiplying both sides by the same expression never changes the solution set → reject — Multiplying x=2 by 0 gives 0=0, and the solution set grows from {2} to ℝ; here multiplying by x−1 also adds the solution 1 (S14).
• x²/(x−1) is itself an equation → reject — It has no equality sign; it is an expression (one side of the equation), and without a second side there is no solution set.

Result and limitations

In ℝ, the solution set of x²/(x−1)=1/(x−1) is {−1}. Both sides are defined only for x≠1; there the equation is equivalent to x²=1, that is x=1 or x=−1, and x=1 is outside the domain. The equation x²=1 obtained by multiplying by x−1 has solutions {−1,1}; the extra 1 is exactly where the multiplier x−1 vanishes.

• This guide treats one concrete equation; general rational equations (several denominators, higher-degree numerators) need the same tracking of the domain, which is not proved here.
• The zero-product property and the fraction rules are used as premises from the glossary and are not derived here from the field axioms.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 70e4d5766cd19e87cc7a8b9f5a847402b534f1a14a56165b9364b027e1664496
• original source SHA-256: 105cc4d24c32a42632c2fa35bdefc5573f9ebff81adc1112f41ccac5a8a97832
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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