mathlib3 documentation

mathlib-archive / imo.imo2013_q1

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 #

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 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))