IMO 2015 N3

Let $m$ and $n > 1$ be positive integers such that $k ∣ m$ whenever $n ≤ k < 2n$. Prove that $L - 1$ is not a power of $2$, where $$ L = \prod_{k = n}^{2n - 1} \left(\frac{m}{k} + 1\right). $$

theorem IMOSL.IMO2015N3.div_pos_of_dvd {m k : ℕ} (hm : 0 < m) (hk : k ∣ m) : 0 < m / k

theorem IMOSL.IMO2015N3.clog_base_mul {b n : ℕ} (hb : 1 < b) (hn : 0 < n) : Nat.clog b (b * n) = Nat.clog b n + 1

theorem IMOSL.IMO2015N3.two_pow_clog_mem_Ico {n : ℕ} (hn : 0 < n) : 2 ^ Nat.clog 2 n ∈ Finset.Ico n (2 * n)

theorem IMOSL.IMO2015N3.prod_mod_ne_one {ι : Type u_1} {n : ℕ} [DecidableEq ι] {I : Finset ι} {f : ι → ℕ} (h : ∃ i₀ ∈ I, ∀ i ∈ I, n ∣ f i ↔ i ≠ i₀) : (∏ i ∈ I, (f i + 1)) % n ≠ 1 % n

theorem IMOSL.IMO2015N3.main_lemma {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (h : ∀ k ∈ Finset.Ico n (2 * n), k ∣ m) : ∃ (t : ℕ), ∀ k ∈ Finset.Ico n (2 * n), 2 ^ t ∣ m / k ↔ k ≠ 2 ^ Nat.clog 2 n

theorem IMOSL.IMO2015N3.final_solution {m n : ℕ} (hm : 0 < m) (hn : 1 < n) (h : ∀ k ∈ Finset.Ico n (2 * n), k ∣ m) (N : ℕ) : ∏ k ∈ Finset.Ico n (2 * n), (m / k + 1) ≠ 2 ^ N + 1

Final solution