Prove2Me

lean_workbook_plus_69758

Proved

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

This is easy.Rewrite the ineq as\n\n a(c+1)+b(a+1)+c(b+1)(a+1)(b+1)(c+1)≥34\frac{a(c+1)+b(a+1)+c(b+1)}{(a+1)(b+1)(c+1)}\ge \frac{3}{4}\n\n ⇔1−1+abc(a+1)(b+1)(c+1)≥34\Leftrightarrow 1-\frac{1+abc}{(a+1)(b+1)(c+1)}\ge \frac{3}{4}\n\n ⇔(a+1)(b+1)(c+1)≥8\Leftrightarrow (a+1)(b+1)(c+1)\ge 8 now this follows from multiplying the inequalities a+1≥2a,b+1≥2b,c+1≥2ca+1\ge 2\sqrt{a},b+1\ge 2\sqrt{b},c+1\ge 2\sqrt{c} and abc=1abc=1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69758  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a * b * c = 1) :
  (a + 1) * (b + 1) * (c + 1) ≥ 8   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph