Documentation

Archive.Imo.Imo2019Q4

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 = iFinset.range n, (2 ^ n - 2 ^ i)) :
n < 6
theorem imo2019_q4 {k : } {n : } (hk : k > 0) (hn : n > 0) :
k.factorial = iFinset.range n, (2 ^ n - 2 ^ i) (k, n) = (1, 1) (k, n) = (3, 2)