lean_workbook_plus_50338

Proved

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

Have $|a^3|\le bc\Rightarrow a^6 + b^6 + c^6 = b^6 + c^6 + (a^3)^2\le b^6 + c^6 + b^2c^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50338 (a b c : ℝ) : |a^3| ≤ b * c → a^6 + b^6 + c^6 ≤ b^6 + c^6 + b^2 * c^2   :=  by sorry

Source