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.prod_lemma
(m : ℕ → ℕ+)
(k : ℕ)
(nm : ℕ+)
:
(Finset.prod (Finset.range k) fun i => 1 + 1 / ↑↑(if i < k then m i else nm)) = Finset.prod (Finset.range k) fun i => 1 + 1 / ↑↑(m i)
theorem
imo2013_q1
(n : ℕ+)
(k : ℕ)
:
∃ m, 1 + (2 ^ k - 1) / ↑↑n = Finset.prod (Finset.range k) fun i => 1 + 1 / ↑↑(m i)