lean_workbook_plus_358

Proved

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

Let $x$ be an integer. What is the smallest possible value of $|2x - 7| + |2x - 9| + |2x - 11| + |2x - 13| + |2x - 15|$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_358 (x : ℤ) : 13 ≤ |2*x - 7| + |2*x - 9| + |2*x - 11| + |2*x - 13| + |2*x - 15|   :=  by sorry

Source