Main derivation
S01 · definition
Before
L(x)=R(x)\ \text{over}\ \mathbb{R}After
\mathcal{S}=\{x\in\mathbb{R}\mid L(x),R(x)\ \text{defined}\ \land\ L(x)=R(x)\}Conditions: none
Rule: mko_equation · Uses: G1, G2, G3
Leaf basis: mko_equation + set_builder
By the MKO, the solution set is not 'the numbers that make the formulas look equal' but the allowed x satisfying two conditions at once: both sides are defined, and their values are equal. Here the allowed domain is ℝ with real operations (G1). Every later step must keep track of both conditions, 'defined' and 'equal'.
S02 · equivalent
Before
L(x)\ \text{and}\ R(x)\ \text{defined}After
x-1\neq 0
Conditions: none
Rule: mul_inverse_nonzero · Uses: G1, G2
Leaf basis: mul_inverse_nonzero + def_unfold
L(x)=x²/(x−1) and R(x)=1/(x−1) each contain one division, both with divisor x−1; the numerators x² and 1 are defined for every real. By mul_inverse_nonzero, v/u is defined exactly when u≠0, so both sides are defined ⇔ x−1≠0.
S03 · equivalent
Before
x-1\neq 0
After
x\neq 1;\quad D=\{x\in\mathbb{R}\mid x\neq 1\}Conditions: none
Rule: L_zero_diff · Uses: S02
Leaf basis: eq_congruence + add_assoc + add_inverse + add_zero
By Lemma L_zero_diff (u=x, c=1), x−1=0 ⇔ x=1; negating both sides gives x−1≠0 ⇔ x≠1. So the x at which both sides are defined form exactly D={x∈ℝ ∣ x≠1}, and 𝒮⊆D.
S04 · equivalent
Before
\frac{x^2}{x-1}=\frac{1}{x-1},\ x\in DAfter
x^2=1,\ x\in D
Conditions: x-1\neq 0
Rule: L_den · Uses: S03, G2
Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc + mul_one
For x∈D, x−1≠0. By Lemma L_den (a=x², b=1, u=x−1): x²/(x−1)=1/(x−1) ⇔ x²=1. This equivalence holds only in D: its hypothesis u≠0 is exactly x∈D.
S05 · equivalent
Before
x^2=1
After
x^2-1=0
Conditions: none
Rule: L_zero_diff · Uses: S04
Leaf basis: eq_congruence + add_inverse + add_assoc + add_zero
By Lemma L_zero_diff (u=x², c=1): x²−1=0 ⇔ x²=1. Bringing the equation to the form 'expression = 0' is what allows the zero-product property.
S06 · equivalent
Before
x^2-1=0
After
(x-1)(x+1)=0
Conditions: none
Rule: distributive · Uses: S05
Leaf basis: distributive + neg_mul + add_inverse + eq_replace
By distributivity: (x−1)(x+1)=x·x+x·1−1·x−1·1=x²+x−x−1=x²−1. The two expressions are equal for every real, so replacing one by the other does not change whether the equation holds.
S07 · equivalent
Before
(x-1)(x+1)=0
After
x-1=0\ \lor\ x+1=0
Conditions: none
Rule: zero_product · Uses: S06
Leaf basis: zero_product
By the zero-product property (ℝ has no zero divisors): a product of two reals is 0 exactly when at least one factor is 0.
S08 · equivalent
Before
x-1=0\ \lor\ x+1=0
After
x=1\ \lor\ x=-1
Conditions: none
Rule: L_zero_diff · Uses: S07
Leaf basis: eq_congruence + add_inverse + add_zero + numeric_evaluation
By Lemma L_zero_diff: x−1=0 ⇔ x=1; also x+1=x−(−1), so x+1=0 ⇔ x=−1. Each disjunct is transformed by an equivalence, so the disjunction before and after is true or false together.
S09 · equivalent
Before
x\in D:\ L(x)=R(x)
After
\mathcal{S}=\{x\in\mathbb{R}\mid x\in D\ \land\ (x=1\lor x=-1)\}Conditions: x\in D
Rule: logic_chain · Uses: S01, S03, S04, S05, S06, S07, S08
Leaf basis: logic_chain + set_builder
Each of S04 to S08 is an equivalence under the condition x∈D; chaining them gives, for x∈D, L(x)=R(x) ⇔ x=1 ∨ x=−1. Together with S01 and S03 ('defined' ⇔ x∈D), 𝒮={x∈ℝ ∣ x∈D and (x=1 or x=−1)}.
S10 · implies
Before
x=1
After
1\notin D,\ \text{so}\ 1\notin\mathcal{S}Conditions: none
Rule: set_builder · Uses: S03, S09
Leaf basis: set_builder + numeric_evaluation
Candidate x=1: 1−1=0, so 1∉D, and L(1) and R(1) both involve division by 0 and are undefined. By the set condition of S09, 1∉𝒮. This candidate satisfies x²=1 but is not in the solution set of the original equation.
S11 · implies
Before
x=-1
After
-1\in D,\ \text{so}\ -1\in\mathcal{S}Conditions: -1-1\neq 0
Rule: set_builder · Uses: S03, S09
Leaf basis: set_builder + numeric_evaluation
Candidate x=−1: −1−1=−2≠0, so −1∈D; and x=−1 satisfies the second disjunct. By the set condition of S09 both conjuncts hold, so −1∈𝒮.
S12 · implies
Before
x\in\mathcal{S}\iff x\in D\land(x=1\lor x=-1)After
\mathcal{S}=\{-1\}Conditions: none
Rule: set_extensionality · Uses: S09, S10, S11
Leaf basis: set_extensionality + case_analysis
For any x: if x∈𝒮 then x∈D and x=1 or x=−1; x=1 is incompatible with x∈D (S10), so x=−1. Conversely x=−1 gives x∈𝒮 (S11). The two inclusions together give 𝒮={−1} by set equality.
S13 · implies
Before
x=-1\ \text{in}\ L,\ RAfter
L(-1)=\frac{1}{-2}=-\tfrac{1}{2}=R(-1)Conditions: none
Rule: numeric_evaluation · Uses: S12, G2
Leaf basis: numeric_evaluation + frac_rules
By the MKO, a candidate is checked by substituting it into the original equation and computing each side: L(−1)=(−1)²/(−1−1)=1/(−2)=−1/2 and R(−1)=1/(−1−1)=−1/2. Both sides are defined and equal, in agreement with S12.
S14 · implies
Before
\{x\in\mathbb{R}\mid x^2=1\}After
\{-1,1\}\supsetneq\mathcal{S}=\{-1\}Conditions: none
Rule: set_extensionality · Uses: S05, S06, S07, S08, S12
Leaf basis: set_extensionality + logic_chain
If the domain is ignored and x²=1 is solved on all of ℝ after multiplying by x−1, the equivalences S05 to S08 (which do not depend on x∈D) give {−1,1}. The extra 1 is exactly where the multiplier x−1 is 0: multiplying by x−1 carries solutions of the original equation to the new one, but where x−1=0 one cannot multiply by 1/(x−1) to come back, so the new equation gains a solution that the original does not have.
S15 · implies
Before
\mathcal{S}=\{-1\},\ \{x\mid x^2=1\}=\{-1,1\}After
\text{answer: }\mathcal{S}=\{-1\};\ 1\ \text{excluded since}\ 1\notin DConditions: none
Rule: and_intro_elim · Uses: S12, S13, S14
Leaf basis: and_intro_elim
The solution set of x²/(x−1)=1/(x−1) in ℝ is {−1}; the other solution 1 of x²=1 is excluded because both sides are undefined at x=1.
Substeps and lemmas
S03.1 · equivalent
Before
u-c=0
After
(u-c)+c=0+c
Conditions: none
Rule: eq_congruence · Uses: eq_congruence
Leaf basis: eq_congruence + add_inverse
Add c to both sides. The backward move is to add −c to both sides and simplify in the same way as S03.2.
S03.2 · equivalent
Before
(u-c)+c=0+c
After
u=c
Conditions: none
Rule: eq_replace · Uses: S03.1
Leaf basis: add_assoc + add_comm + add_inverse + add_zero + eq_replace
The left side is (u+(−c))+c=u+((−c)+c)=u+0=u (meaning of u−c, associativity, commutativity, inverses, identity); the right side is 0+c=c. S03.1 and S03.2 together prove Lemma L_zero_diff.
S04.1 · equivalent
Before
\frac{a}{u}=\frac{b}{u}After
\frac{a}{u}\cdot u=\frac{b}{u}\cdot uConditions: u\neq 0
Rule: eq_congruence · Uses: eq_congruence, mul_inverse_nonzero
Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc
Forwards: multiply both sides by u. Backwards: multiply both sides by 1/u, which needs u≠0, because ((a/u)u)(1/u)=(a/u)(u·(1/u))=a/u. So the two equations are equivalent when u≠0.
S04.2 · equivalent
Before
\frac{a}{u}\cdot u=\frac{b}{u}\cdot uAfter
a=b
Conditions: u\neq 0
Rule: eq_replace · Uses: S04.1
Leaf basis: mul_assoc + mul_comm + mul_inverse_nonzero + mul_one + eq_replace
Using a/u=a·(1/u): (a·(1/u))u=a((1/u)u)=a·1=a; the right side gives b in the same way. S04.1 and S04.2 together prove Lemma L_den.