IMO 2006 N5

Determine all pairs $(x, y)$ of integers such that $$ \sum_{k = 0}^6 x^k = y^5 - 1. $$

Answer

No such pairs.

Solution

We follow the official solution. We show more: for any prime $p > 3$, there exist no pairs $(x, y)$ of integers with $$ \sum_{k = 0}^{p - 1} x^k = y^{p - 2} - 1. $$ We formalize this stronger version instead of the original version. We modify the solution in the case $y ≡ 2 \pmod{p}$ a bit; instead of looking at $y^{p - 3} + y^{p - 4} + … + 1$ mod $p$, we look at $y^{p - 2} - 1$ mod $p$.

theorem IMOSL.IMO2006N5.FiniteField_prime_geom_sum_eq_zero_imp {F : Type u_1} {p : ℕ} [Field F] [Fintype F] [DecidableEq F] (hp : Nat.Prime p) {x : F} (hx : x ≠ 1) (hx0 : ∑ i ∈ Finset.range p, x ^ i = 0) : Fintype.card F ≡ 1 [MOD p]

Let p be a prime and F be a finite field. Suppose that there exists x : F with x ≠ 1 such that ∑_{i = 0}^{p - 1} x^i = 0. Then |F| ≡ 1 (mod p).

theorem IMOSL.IMO2006N5.Nat_prime_dvd_prime_geom_sum_imp {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) {x : ℤ} (hx : ↑p ∣ ∑ i ∈ Finset.range q, x ^ i) : p = q ∨ p ≡ 1 [MOD q]

Let p and q be prime with p ∣ ∑_{i = 0}^{q - 1} x^i for sone x : ℤ. Then p is either equal to q or congruent to 1 (mod q).

theorem IMOSL.IMO2006N5.Nat_dvd_prime_geom_sum_imp {p : ℕ} (hp : Nat.Prime p) {d : ℕ} {x : ℤ} (hx : ↑d ∣ ∑ i ∈ Finset.range p, x ^ i) : p ∣ d ∨ d ≡ 1 [MOD p]

Let d : ℕ and p be prime with d ∣ ∑_{i = 0}^{p - 1} x^i for sone x : ℤ. Then either p ∣ d or d ≡ 1 (mod p).

theorem IMOSL.IMO2006N5.Int_dvd_prime_geom_sum_imp {p : ℕ} (hp : Nat.Prime p) {d : ℤ} (hd : d ≥ 0) {x : ℤ} (hx : d ∣ ∑ i ∈ Finset.range p, x ^ i) : ↑p ∣ d ∨ d ≡ 1 [ZMOD ↑p]

Let d ≥ 0 and p be prime with d ∣ ∑_{i = 0}^{p - 1} x^i for sone x : ℤ. Then either p ∣ d or d ≡ 1 (mod p).

theorem IMOSL.IMO2006N5.Int_dvd_prime_geom_sum_imp_ZMod {p : ℕ} (hp : Nat.Prime p) {d : ℤ} (hd : d ≥ 0) {x : ℤ} (hx : d ∣ ∑ i ∈ Finset.range p, x ^ i) : ↑d = 0 ∨ ↑d = 1

Let d ≥ 0 and p be prime with d ∣ ∑_{i = 0}^{p - 1} x^i for sone x : ℤ. Then in ZMod p, d is either equal to 0 or 1.

theorem IMOSL.IMO2006N5.final_solution {p : ℕ} (hp : Nat.Prime p) (hp0 : p > 3) (x y : ℤ) : ¬∑ i ∈ Finset.range p, x ^ i = y ^ (p - 2) - 1

Final solution