lean_workbook_plus_77409

Proved

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

Let $S_n = 4^{n+1} + 5^{2n-1}$ . If $21 | S_k = 4^{k+1} + 5^{2k-1}$ , then \n\n $S_{k+1} = 4^{k+2} + 5^{2k+1} = 4 \cdot 4^{k+1} + 25 \cdot 5^{2k-1} = 4S_k + 21 \cdot 5^{2k-1}$ \n\n so $21 | S_{k+1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77409  (n : ℕ)
  (h₀ : 21 ∣ (4^(n + 1) + 5^(2 * n - 1))) :
  21 ∣ (4^(n + 2) + 5^(2 * n + 1))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph