IMO 2008 Q2

(a) Prove that x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1 ``` for all real numbers x,y, z, each different from 1, and satisfying xyz = 1.

(b) Prove that equality holds above for infinitely many triples of rational numbers x, y, z, each different from 1, and satisfying xyz = 1.

Solution

(a) Since xyz = 1, we can apply the substitution x = a/b, y = b/c, z = c/a. Then we define m = c-b, n = b-a and rewrite the inequality as LHS - 1 ≥ 0 using c, m and n. We factor LHS - 1 as a square, which finishes the proof.

(b) We present a set W of rational triples. We prove that W is a subset of the set of rational solutions to the equation, and that W is infinite.

theorem Imo2008Q2.subst_abc {x y z : ℝ} (h : x * y * z = 1) : ∃ (a : ℝ) (b : ℝ) (c : ℝ), a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a / b ∧ y = b / c ∧ z = c / a

theorem Imo2008Q2.imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠ 1) (hz : z ≠ 1) : x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1

def Imo2008Q2.rationalSolutions : Set (ℚ × ℚ × ℚ)

Equations

• One or more equations did not get rendered due to their size.

theorem Imo2008Q2.imo2008_q2b : rationalSolutions.Infinite