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 IMO2005Q4.a (n : ℕ) : ℤ

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

Equations

• IMO2005Q4.a n = 2 ^ n + 3 ^ n + 6 ^ n - 1

theorem IMO2005Q4.find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) : ↑p ∣ IMO2005Q4.a (p - 2)

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

theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ (n : ℕ), 1 ≤ n → IsCoprime (IMO2005Q4.a n) ↑k) ↔ k = 1

Main statement: The only positive integer coprime to all terms of the sequence a is 1.