IMO 2019 Q4 #
Find all pairs (k, n) of positive integers such that
k! = (2 ^ n - 1)(2 ^ n - 2)(2 ^ n - 4)···(2 ^ n - 2 ^ (n - 1))
We show in this file that this property holds iff (k, n) = (1, 1) ∨ (k, n) = (3, 2).
Proof sketch:
The idea of the proof is to count the factors of 2 on both sides. The LHS has less than k factors
of 2, and the RHS has exactly n * (n - 1) / 2 factors of 2. So we know that n * (n - 1) / 2 < k.
Now for n ≥ 6 we have RHS < 2 ^ (n ^ 2) < (n(n-1)/2)! < k!. We then treat the cases n < 6
individually.
theorem
Imo2019Q4.upper_bound
{k n : ℕ}
(hk : k > 0)
(h : ↑k.factorial = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i))
:
n < 6