Latvian National Olympiad 2025 Grade 12 Problem 1

Prove that for all positive integers $n$, $2^{2n-1} 3^{n-1} + 5^n$ is divisible by $7$.

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Data.Nat.Basic

theorem solution (n : ℕ) (hn : n > 0) : 7 ∣ 2 ^ (2 * n - 1) * 3 ^ (n - 1) + 5 ^ n := sorry

Login to submit a solution.