Prove2Me

Lean-Workbook Plus 57988: Trigonometric inequality

Proved
WorkbookRestored.plus_57988

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every integer nn, 24cos⁡4(nπ/9)≤9cos⁡2(nπ/9)+16cos⁡6(nπ/9)24\cos^4(n\pi/9)\le9\cos^2(n\pi/9)+16\cos^6(n\pi/9).

Source: Lean-Workbook row lean_workbook_plus_57988 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_57988 (n : ℤ) : 24 * (cos (n * π / 9))^4 ≤ 9 * (cos (n * π / 9))^2 + 16 * (cos (n * π / 9))^6   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_57988; immutable original Prove2Me node 4b1c4a04-2431-4c24-a620-75d90290e216

View graph