IMO 2013 Q1 #

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

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 #

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

theorem imo2013_q1.arith_lemma (k n : ℕ) :

0 < 2 * n + 2 ^ k.succ

theorem imo2013_q1.prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :

(finset.range k).prod (λ (i : ℕ), 1 + 1 / ↑(ite (i < k) (m i) nm)) = (finset.range k).prod (λ (i : ℕ), 1 + 1 / ↑(m i))

theorem imo2013_q1 (n : ℕ+) (k : ℕ) :

∃ (m : ℕ → ℕ+), 1 + (2 ^ k - 1) / ↑n = (finset.range k).prod (λ (i : ℕ), 1 + 1 / ↑(m i))