IMO 2005 Q4 #

Problem: Determine all positive integers relatively prime to all the terms of the infinite sequence a n = 2 ^ n + 3 ^ n + 6 ^ n - 1, for n ≥ 1.

This is quite an easy problem, in which the key point is a modular arithmetic calculation with the sequence a n relative to an arbitrary prime.

def a (n : ℕ) :

The sequence considered in the problem, 2 ^ n + 3 ^ n + 6 ^ n - 1.

Equations

theorem find_specified_factor {p : ℕ} (hp : nat.prime p) (hp' : is_coprime 6 ↑p) :

↑p ∣ a (p - 2)

Key lemma (a modular arithmetic calculation): Given a prime p other than 2 or 3, the p - 2th term of the sequence has p as a factor.