A Number Theory Problem

Let $a$, $b$, and $n$ be positive integers with $a > b > 1$. Suppose that $b$ is odd and that $b^n$ divides $a^n - 1$. Show that $a ^ b > \frac{3 ^ n}{n}$.

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

import Mathlib.Algebra.Ring.Parity

theorem solution {a b n : ℕ} (hs : a > b ∧ b > 1) (hn : n > 0) (ho : Odd b)
    (hd : b ^ n ∣ a ^ n - 1) : n * a ^ b > 3 ^ n := sorry

Submit Solution

Login to submit a solution.

Recent Submissions