mathlib3 documentation

mathlib-archive / imo.imo2005_q4

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.

def imo2005_q4.a (n : ) :

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

Equations
theorem imo2005_q4.find_specified_factor {p : } (hp : nat.prime p) (hp' : is_coprime 6 p) :

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.