lean_workbook_plus_57089

Proved

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

We have to prove that: \n $(b^2+2)(c^2+2)\geq 3\left [ 1+\frac{(b+c)^2}{2} \right ]\Leftrightarrow (bc-1)^2+\frac{(b-c)^2}{2}\geq 0$ (true)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57089 (b c : ℝ) : (b^2 + 2) * (c^2 + 2) ≥ 3 * (1 + (b + c)^2 / 2) ↔ (b * c - 1)^2 + (b - c)^2 / 2 ≥ 0   :=  by sorry

Source