IMO 2005 Q4 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
theorem
imo2005_q4.find_specified_factor
{p : ℕ}
(hp : nat.prime p)
(hp' : is_coprime 6 ↑p) :
↑p ∣ imo2005_q4.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.
theorem
imo2005_q4
{k : ℕ}
(hk : 0 < k) :
(∀ (n : ℕ), 1 ≤ n → is_coprime (imo2005_q4.a n) ↑k) ↔ k = 1
Main statement: The only positive integer coprime to all terms of the sequence a is 1.