Documentation

IMOSLLean4.Main.IMO2008.N1

IMO 2008 N1 #

Let $m, n, p$ be non-negative integers with $m$ odd and $p$ prime. Let $x_1, x_2, …, x_m$ be integers such that $$ x_1^n + px_2 = x_2^n + px_3 = … = x_m^n + px_1. $$ Prove that $x_1 = x_2 = … = x_n$.

Solution #

We follow Solution 2 of the official solution, with some shortcuts made along the way. For $n$ odd, we show that $x_i < x_{i + 2}$ implies $x_{i + 2} < x_{i + 4}$, and similarly $x_i > x_{i + 2}$ implies $x_{i + 2} > x_{i + 4}$. In particular, $p$ only needs to either be odd or equal to $±2$; the above modification makes sure that the solution works even when $p < 0$. Our implementation will also assume $p$ is either odd or $±2$ instead of being prime. For the case $p = ±2$, $n = 2k$, after showing $|x_i^k + x_{i + 1}^k| = 2$, we deduce $x_{i + 1}^k = x_{i - 1}^k$ for some $i$ and then get $x_{i + 2} = x_i$.

Notes #

The original problem considers $m = 3$, but the same method works for any odd $m$. However, the statement is false when $p = 4$ and $m = 3$. A counterexample is given by $(x_1, x_2, x_3) = (7, -5, 1)$ with $n = 2$.

Extra lemmas #

theorem IMOSL.IMO2008N1.odd_of_dvd_Int {a b : } (ha : Odd b) (hab : a b) :
Odd a

If a ∣ b and b is odd, then a is odd.

theorem IMOSL.IMO2008N1.mul_eq_one_Nat {m n : } :
m * n = 1 m = 1 n = 1

Given natural numbers m and n, we have mn = 1 iff m = 1 and n = 1.

theorem IMOSL.IMO2008N1.odd_prod_Int {ι : Type u_1} [DecidableEq ι] {f : ι} {I : Finset ι} :
Odd (∏ iI, f i) iI, Odd (f i)

The product of several integers is odd iff each term is odd.

theorem IMOSL.IMO2008N1.odd_prod_Int_Fintype {ι : Type u_1} [DecidableEq ι] [Fintype ι] {f : ι} :
Odd (∏ i : ι, f i) ∀ (i : ι), Odd (f i)

The product of several integers is odd iff each term is odd.

theorem IMOSL.IMO2008N1.prod_eq_one_Nat {ι : Type u_1} [DecidableEq ι] {f : ι} {I : Finset ι} :
iI, f i = 1 iI, f i = 1

If the product of several natural numbers is one, then each term is one.

theorem IMOSL.IMO2008N1.prod_eq_one_Nat_Fintype {ι : Type u_1} [DecidableEq ι] [Fintype ι] {f : ι} :
i : ι, f i = 1 ∀ (i : ι), f i = 1

If the product of several natural numbers is one, then each term is one.

theorem IMOSL.IMO2008N1.natAbs_prod_Int {ι : Type u_1} [DecidableEq ι] (f : ι) (I : Finset ι) :
(∏ iI, f i).natAbs = iI, (f i).natAbs

The natAbs of product is equal to the product of natAbs.

Start of the problem #

def IMOSL.IMO2008N1.good (m n : ) (p : ) [NeZero m] (x : Fin m) :

A sequence x_1, x_2, …, x_m of integers is called (n, p)-good if x_i^n + px_{i + 1} = x_j^n + px_{j + 1} holds for any i : ℕ.

Equations
Instances For
    theorem IMOSL.IMO2008N1.good.map_add_eq_of_map_eq {m : } [NeZero m] {n : } {p : } (hp : p 0) {x : Fin m} (hx : good m n p x) {i j : Fin m} (hx0 : x i = x j) (k : Fin m) :
    x (i + k) = x (j + k)

    Suppose p ≠ 0, and let (x_i) be an (n, p)-good sequence. If x_i = x_j, then x_{i + k} = x_{j + k} for any k.

    theorem IMOSL.IMO2008N1.good.map_add_nat_mul_of_map_add_nat_eq {m : } [NeZero m] {n : } {p : } (hp : p 0) {x : Fin m} (hx : good m n p x) {i : Fin m} {j : } (hx0 : x (i + j) = x i) (k : ) :
    x (i + ↑(j * k)) = x i

    Suppose p ≠ 0, and let (x_i) be an (n, p)-good sequence. If x_{i + j} = x_i, then x_{i + jk} = x_i for any k.

    theorem IMOSL.IMO2008N1.good.const_of_exists_map_add_one_eq {m : } [NeZero m] {n : } {p : } (hp : p 0) {x : Fin m} (hx : good m n p x) (hx0 : ∃ (i : Fin m), x (i + 1) = x i) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If p ≠ 0 and (x_i) is an (n, p)-good sequence such that x_{i + 1} = x_i for some i, then (x_i) is constant.

    theorem IMOSL.IMO2008N1.good.const_of_exists_map_add_two_eq {m : } [NeZero m] {p : } {n : } {x : Fin m} (hm : Odd m) (hp : p 0) (hx : good m n p x) (hx0 : ∃ (i : Fin m), x (i + 2) = x i) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If p ≠ 0 and (x_i) is an (n, p)-good sequence of odd length such that x_{i + 2} = x_i for some i, then (x_i) is constant.

    theorem IMOSL.IMO2008N1.good.neg_of_exp_odd {m : } [NeZero m] {n : } (hn : Odd n) {p : } {x : Fin m} (hx : good m n p x) :
    good m n p (-x)

    If n is odd and (x_i) is (n, p)-good, then (-x_i) is (n, p)-good.

    theorem IMOSL.IMO2008N1.good.const_of_exp_odd_p_nonpos {m : } [NeZero m] {n : } (hn : Odd n) {p : } (hp : p 0) {x : Fin m} (hx : good m n p x) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If n is odd and p ≤ 0, then any (n, p)-good sequence is constant.

    theorem IMOSL.IMO2008N1.good.two_periodic_of_exp_odd_p_pos {m : } [NeZero m] {n : } (hn : Odd n) {p : } (hp : p > 0) {x : Fin m} (hx : good m n p x) (i : Fin m) :
    x (i + 2) = x i

    If n is odd and p > 0, then any (n, p)-good sequence is 2-periodic.

    theorem IMOSL.IMO2008N1.good.const_of_exp_odd_length_odd {m : } [NeZero m] {n : } (hn : Odd n) {p : } (hm : Odd m) {x : Fin m} (hx : good m n p x) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If n is odd, then any (n, p)-good sequence of odd length is constant.

    theorem IMOSL.IMO2008N1.good.formula_of_exp_two_mul {m : } [NeZero m] {k : } {p : } {x : Fin m} (hx : good m (2 * k) p x) :
    (∏ i : Fin m, (x i ^ k + x (i + 1) ^ k)) * i : Fin m, (x i ^ k - x (i + 1) ^ k) = (-p) ^ m * i : Fin m, (x i - x (i + 1))

    A general formula for (2k, p)-good sequences.

    theorem IMOSL.IMO2008N1.good.formula_of_exp_two_mul2 {m : } [NeZero m] {k : } {p : } {x : Fin m} (hx : good m (2 * k) p x) (hx0 : ∀ (i : Fin m), x (i + 1) x i) :
    (∏ i : Fin m, (x i ^ k + x (i + 1) ^ k)) * i : Fin m, (x i ^ k - x (i + 1) ^ k) / (x i - x (i + 1)) = (-p) ^ m

    A general formula for (2k, p)-good sequences with adjacent terms being distinct.

    theorem IMOSL.IMO2008N1.good.dvd_of_exp_two_mul {m : } [NeZero m] {k : } {p : } {x : Fin m} (hx : good m (2 * k) p x) (hx0 : ∀ (i : Fin m), x (i + 1) x i) :
    i : Fin m, (x i ^ k + x (i + 1) ^ k) p ^ m

    If (x_i) is a (2k, p)-good sequence with adjacent terms being distinct, then ∏_i (x_i^k + x_{i + 1}^k) ∣ p^m.

    theorem IMOSL.IMO2008N1.good.const_of_exp_two_mul_and_p_odd {m : } [NeZero m] {k : } {p : } (hm : Odd m) (hp : Odd p) {x : Fin m} (hx : good m (2 * k) p x) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If p is odd, then any (2k, p)-good sequence of odd length is constant.

    theorem IMOSL.IMO2008N1.good.neg_of_exp_even {m : } [NeZero m] {k : } {p : } {x : Fin m} (hx : good m (2 * k) p x) :
    good m (2 * k) (-p) (-x)

    If (x_i) is a (2k, p)-good sequence, then (-x_i) is (2k, -p)-good.

    theorem IMOSL.IMO2008N1.good.const_of_exp_two_mul_and_abs_p_eq_two {m : } [NeZero m] {k : } {p : } (hm : Odd m) (hp : p.natAbs = 2) {x : Fin m} (hx : good m (2 * k) p x) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    If |p| = 2, then any (2k, p)-good sequence of odd length is constant.

    theorem IMOSL.IMO2008N1.final_solution {m n : } {p : } [NeZero m] (hm : Odd m) (hp : Odd p p.natAbs = 2) {x : Fin m} (hx : good m n p x) :
    ∃ (C : ), ∀ (i : Fin m), x i = C

    Final solution