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) ≤ 8xyz.

We then reparametrize x = q + r, y = r + p, z = p + q where p, q, r ∈ ℝ, which transforms the inequality to 8pqr ≤ (q + r)(r + p)(p + q).

The proof splits into cases based on the signs of p, q, r. When all are positive, AM-GM gives the result. When at least one is negative or zero, the inequality is verified by sign analysis.

Implementation notes

• The inequality is reduced via A = x / y, B = y / z, C = z / x, then the substitution x = q + r, y = r + p, z = p + q.
• Helper lemmas prove 8pqr ≤ (p + q)(r + p)(q + r) by AM-GM when p, q, r > 0 and by sign analysis otherwise; the main proof closes with grind.

References

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

theorem Imo2000Q2.eight_mul_le_prod_add_of_pos {p q r : ℝ} (p_pos : 0 < p) (q_pos : 0 < q) (r_pos : 0 < r) : 8 * p * q * r ≤ (p + q) * (q + r) * (r + p)

When p, q, r > 0, 8pqr ≤ (p + q)(r + p)(q + r), by writing the difference of squares as a sum of nonnegative squares.

theorem Imo2000Q2.eight_mul_le_prod_add_of_nonpos {p q r : ℝ} (p_nonpos : p ≤ 0) (r_pos : 0 < r) (q_pos : 0 < q) (p_add_q_pos : 0 < p + q) (r_add_p_pos : 0 < r + p) : 8 * p * q * r ≤ (p + q) * (r + p) * (q + r)

When p ≤ 0 but q, r > 0 and both pairwise sums are positive, the left side is nonpositive so the inequality holds.

theorem Imo2000Q2.eight_mul_le_prod_add_of_add_pos (p q r : ℝ) (hpq : 0 < p + q := by grind) (hqr : 0 < q + r := by grind) (hrp : 0 < r + p := by grind) : 8 * p * q * r ≤ (p + q) * (q + r) * (r + p)

When all three pairwise sums p + q, r + p, q + r are positive, the inequality holds by casing on the signs of p, q, r.

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.