lean_workbook_plus_17988

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that for $x, y, z> 0$ \n $\frac{x^2y^2+z^2y^2+x^2z^2}{xyz}\geq x+y+z$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17988 : ∀ x y z : ℝ, x > 0 ∧ y > 0 ∧ z > 0 → (x^2*y^2 + z^2*y^2 + x^2*z^2) / (x*y*z) ≥ x + y + z   :=  by sorry

Source