Documentation

Archive.Imo.Imo1985Q2

IMO 1985 Q2 #

Fix a natural number $n ≥ 3$ and define $N=\{1, 2, 3, \dots, n-1\}$. Fix another natural number $j ∈ N$ coprime to $n$. Each number in $N$ is now colored with one of two colors, say red or black, so that:

  1. $i$ and $n-i$ always receive the same color, and
  2. $i$ and $|j-i|$ receive the same color for all $i ∈ N, i ≠ j$.

Prove that all numbers in $N$ must receive the same color.

Solution #

Let $a \sim b$ denote that $a$ and $b$ have the same color. Because $j$ is coprime to $n$, every number in $N$ is of the form $kj\bmod n$ for a unique $1 ≤ k < n$, so it suffices to show that $kj\bmod n \sim (k-1)j\bmod n$ for $1 < k < n$. In this range of $k$, $kj\bmod n ≠ j$, so

def Imo1985Q2.Condition (n j : ) (C : Fin 2) :

The conditions on the problem's coloring C. Although its domain is all of , we only care about its values in Set.Ico 1 n.

Equations
Instances For
    theorem Imo1985Q2.C_mul_mod {n j : } (hn : 3 n) (hj : j Set.Ico 1 n) (cpj : n.Coprime j) {C : Fin 2} (hC : Condition n j C) {k : } (hk : k Set.Ico 1 n) :
    C (k * j % n) = C j

    For 1 ≤ k < n, k * j % n has the same color as j.

    theorem Imo1985Q2.result {n j : } (hn : 3 n) (hj : j Set.Ico 1 n) (cpj : n.Coprime j) {C : Fin 2} (hC : Condition n j C) {i : } (hi : i Set.Ico 1 n) :
    C i = C j