IMO 1964 Q1

(a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.

(b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.

We define a predicate for the solutions in (a), and prove that it is the set of positive integers which are a multiple of 3.

Intermediate lemmas

theorem Imo1964Q1.two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7]

The question

def Imo1964Q1.ProblemPredicate (n : ℕ) : Prop

Equations

• Imo1964Q1.ProblemPredicate n = (7 ∣ 2 ^ n - 1)

theorem Imo1964Q1.imo1964_q1a (n : ℕ) : 0 < n → (Imo1964Q1.ProblemPredicate n ↔ 3 ∣ n)

theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1