lean_workbook_plus_39482

Proved

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

Let $a$ , $b$ , $c$ be three reals such that $c\geq b\geq a\geq 0$ . Prove that $\left(a+3b\right)\left(b+4c\right)\left(c+2a\right)\geq 60abc$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39482 :  ∀ a b c : ℝ, c ≥ b ∧ b ≥ a ∧ a ≥ 0 → (a + 3 * b) * (b + 4 * c) * (c + 2 * a) ≥ 60 * a * b * c   :=  by sorry

Source