# 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
Equations
• One or more equations did not get rendered due to their size.
Instances For