IMO 2013 Q1

Prove that for any pair of positive integers k and n, there exist k positive integers m₁, m₂, ..., mₖ (not necessarily different) such that

1 + (2ᵏ - 1)/ n = (1 + 1/m₁) * (1 + 1/m₂) * ... * (1 + 1/mₖ).

Solution

Adaptation of the solution found in https://www.imo-official.org/problems/IMO2013SL.pdf

We prove a slightly more general version where k does not need to be strictly positive.

theorem Imo2013Q1.arith_lemma (k : ℕ) (n : ℕ) : 0 < 2 * n + 2 ^ k.succ

theorem Imo2013Q1.prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) : ((Finset.range k).prod fun (i : ℕ) => 1 + 1 / ↑↑(if i < k then m i else nm)) = (Finset.range k).prod fun (i : ℕ) => 1 + 1 / ↑↑(m i)

theorem imo2013_q1 (n : ℕ+) (k : ℕ) : ∃ (m : ℕ → ℕ+), 1 + (2 ^ k - 1) / ↑↑n = (Finset.range k).prod fun (i : ℕ) => 1 + 1 / ↑↑(m i)