IMO 2000 Q2

Let A, B, C be positive reals with ABC = 1. Prove that (A - 1 + 1 / B)(B - 1 + 1 / C)(C - 1 + 1 / A) ≤ 1.

Solution

We follow the first solution from https://artofproblemsolving.com/wiki/index.php?title=2000_IMO_Problems/Problem_2.

We parametrize A = x / y, B = y / z, C = z / x where x, y, z > 0. This reduces the problem to proving (x - y + z)(y - z + x)(z - x + y) ≤ xyz.

Writing u = x - y + z, v = y - z + x, w = z - x + y, we have u + v = 2x, v + w = 2y, w + u = 2z, so any two of u, v, w have a positive sum and hence at most one of them can be nonpositive. If one is nonpositive the left-hand side is nonpositive and the inequality is clear. Otherwise all three are positive, and by AM-GM uv ≤ ((u + v) / 2) ^ 2 = x ^ 2, and similarly vw ≤ y ^ 2 and wu ≤ z ^ 2; multiplying these gives (uvw) ^ 2 ≤ (xyz) ^ 2, from which the inequality follows.

References

• https://artofproblemsolving.com/wiki/index.php?title=2000_IMO_Problems/Problem_2

theorem Imo2000Q2.prod_sub_add_le {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x - y + z) * (y - z + x) * (z - x + y) ≤ x * y * z

For positive reals x, y, z we have (x - y + z)(y - z + x)(z - x + y) ≤ xyz.

theorem Imo2000Q2.imo2000_q2 {A B C : ℝ} (A_pos : 0 < A) (B_pos : 0 < B) (C_pos : 0 < C) (h_prod : A * B * C = 1) : (A - 1 + 1 / B) * (B - 1 + 1 / C) * (C - 1 + 1 / A) ≤ 1

IMO 2000 Q2. If A, B, C > 0 and ABC = 1, then (A - 1 + 1 / B)(B - 1 + 1 / C)(C - 1 + 1 / A) ≤ 1.