lean_workbook_plus_70470

Proved

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

Prove that $x^7-3^7x+2.3^7\ge 0$ for $x\ge 3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70470  (x : ℝ)
  (h₀ : 3 ≤ x) :
  x^7 - 3^7 * x + 2 * 3^7 ≥ 0   :=  by sorry

Source