Sequential Divison

Let $a$ be a sequence of natural numbers defined by $a_0 = a_1 = 1$, $a_2 = 2$, and $a_{n + 2} = a_n a_{n + 1} + a_n$ for all natural $n$. Show that for all natural $n \ge 5$, $a_n ^ n$ divides $a_{a_n}$.

Replace sorry in the template below with your solution. Mathlib version used by the checker is v4.34.0.

import Mathlib.Data.Nat.Basic

def a : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | 2 => 2
  | n + 2 => a n * a (n+1) + a n

theorem solution (n : ℕ) (hn : n ≥ 5) : a n ^ n ∣ a (a n) := sorry

Submit Solution

Login to submit a solution.

Recent Submissions