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 #
The question #
def imo1964_q1.problem_predicate (n : ℕ) :
- imo1964_q1.problem_predicate n = (7 ∣ 2 ^ n - 1)
theorem imo1964_q1.aux (n : ℕ) :
theorem imo1964_q1.imo1964_q1a (n : ℕ) (hn : 0 < n) :
imo1964_q1.problem_predicate n ↔ 3 ∣ n