Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2005P3

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2005, Problem 3
Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that:
`(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0`
-/

namespace Imo2005P3

theorem imo2005_p3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
    (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) + (y ^ 5 - y ^ 2) / (y ^ 5 + z ^ 2 + x ^ 2) +
        (z ^ 5 - z ^ 2) / (z ^ 5 + x ^ 2 + y ^ 2) ≥
      0 := sorry


end Imo2005P3

File author(s): Manuel Candales

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2005P3.lean.