IMO 2010 N2

Find all pairs $(m, n) ∈ ℤ × ℕ$ such that $$ m^2 + 2 \cdot 3^n = m(2^{n + 1} - 1). $$

Answer

$(6, 3), (9, 3), (9, 5), (54, 5)$.

Solution

We follow the official solution. While we allow $m$ to be negative, the given equation implies that $m$ is non-negative. For lower bounding $\min\{p, q\}$, we use the LTE (lifting the exponent) lemma instead, giving us the stronger inequality $\min\{p, q\} ≤ \log_3(p + q + 1)$.

def IMOSL.IMO2010N2.good (m : ℤ) (n : ℕ) : Prop

A pair (m, n) is called good if m^2 + 2 3^n = m(2^{n + 1} - 1).

Equations

• IMOSL.IMO2010N2.good m n = (m ^ 2 + 2 * 3 ^ n = m * (2 ^ (n + 1) - 1))

def IMOSL.IMO2010N2.nice (p q : ℕ) : Prop

A pair (p, q) is caled nice if 3^p + 2 3^q = 2^{p + q + 1} - 1.

Equations

• IMOSL.IMO2010N2.nice p q = (3 ^ p + 2 * 3 ^ q = 2 ^ (p + q + 1) - 1)

theorem IMOSL.IMO2010N2.nice.good_three_pow_left {p q : ℕ} (h : nice p q) : good (3 ^ p) (p + q)

Given a nice pair (p, q), the pair (3^p, p + q) is good.

theorem IMOSL.IMO2010N2.nice.good_two_mul_three_pow_right {p q : ℕ} (h : nice p q) : good (2 * 3 ^ q) (p + q)

Given a nice pair (p, q), the pair (2 3^q, p + q) is good.

theorem IMOSL.IMO2010N2.good_iff_nice {m : ℤ} {n : ℕ} : good m n ↔ ∃ (p : ℕ) (q : ℕ), nice p q ∧ n = p + q ∧ (m = 3 ^ p ∨ m = 2 * 3 ^ q)

A pair (m, n) is good iff there exists a nice pair (p, q) such that n = p + q and either m = 3^p or m = 2 3^q.

theorem IMOSL.IMO2010N2.nice.add_le_three_mul_min_add_one {p q : ℕ} (h : nice p q) : p + q ≤ 3 * min p q + 1

If (p, q) is a nice pair, then p + q ≤ 3 min{p, q} + 1.

theorem IMOSL.IMO2010N2.nice.min_pos {p q : ℕ} (h : nice p q) : min p q > 0

If (p, q) is a nice pair, then min{p, q} > 0.

theorem IMOSL.IMO2010N2.two_dvd_of_three_dvd_pow_sub_one {n : ℕ} (h : 3 ∣ 2 ^ n - 1) : 2 ∣ n

If 3 ∣ 2^n - 1, then 2 ∣ n.

theorem IMOSL.IMO2010N2.emultiplicity_three_four_pow_sub_one (r : ℕ) : emultiplicity 3 (4 ^ r - 1) = emultiplicity 3 r + 1

We have ν_3(4^r - 1) = r + 1 for any r : ℕ.

theorem IMOSL.IMO2010N2.multiplicity_three_four_pow_sub_one {r : ℕ} (hr : r ≠ 0) : multiplicity 3 (4 ^ r - 1) = multiplicity 3 r + 1

This lemma is emultiplicity_three_four_pow_sub_one with multiplicity version.

theorem IMOSL.IMO2010N2.nice.add_succ_even_and_min_le_multiplicity {p q : ℕ} (h : nice p q) : ∃ (r : ℕ), p + q + 1 = 2 * r ∧ min p q ≤ multiplicity 3 r + 1

If (p, q) is a nice pair, then p + q + 1 = 2r for some r : ℕ and min{p, q} ≤ ν_3(r) + 1.

theorem IMOSL.IMO2010N2.nice_iff {p q : ℕ} : nice p q ↔ p = 2 ∧ (q = 1 ∨ q = 3)

The only nice pairs are (2, 1) and (2, 3).

theorem IMOSL.IMO2010N2.final_solution {m : ℤ} {n : ℕ} : good m n ↔ n = 3 ∧ (m = 9 ∨ m = 6) ∨ n = 5 ∧ (m = 9 ∨ m = 54)

Final solution