lean_workbook_plus_40695

Proved

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

Prove that for all positive real $x$ , the following inequality holds: \n\n

(x + 1)(x + 2)(x + 5) \geq 36x.

\n\n Note that \n\n $(x + 1)(x + 2)(x + 5) - 36x = (x+10)(x-1)^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40695 (x : ℝ) (h : x > 0) : (x + 1) * (x + 2) * (x + 5) ≥ 36 * x   :=  by sorry

Source