mathlib documentation

mathlib-archive / imo.imo2005_q4

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.