IMO 1964 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

(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 #

2 ^ (3 * m) ≡ 1 [MOD 7]

2 ^ (3 * m + 1) ≡ 2 [MOD 7]

2 ^ (3 * m + 2) ≡ 4 [MOD 7]

Prop

Equations

theorem imo1964_q1.aux (n : ℕ) :

theorem imo1964_q1.imo1964_q1a (n : ℕ) (hn : 0 < n) :

theorem imo1964_q1b (n : ℕ) :

¬7 ∣ 2 ^ n + 1