Documentation

Archive.Imo.Imo2005Q4

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
Instances For
    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 nIsCoprime (IMO2005Q4.a n) k) k = 1

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