lean_workbook_plus_44637

Open

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

Let $a,b,c \in R$ and $a+b+c=0$ . Prove that $\boxed{8^a+8^b+8^c\ge 2^a+2^b+2^c}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44637 : a + b + c = 0 → 8^a + 8^b + 8^c ≥ 2^a + 2^b + 2^c   :=  by sorry

Source