# mathlib3documentation

mathlib-archive / imo.imo2008_q2

# IMO 2008 Q2 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. (a) Prove that lean 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 imo2008_q2.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 imo2008_q2.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