IMO 2007 N1

Find all pairs $(k, n) ∈ ℕ^2$ such that $7^k - 3^n ∣ k^4 + n^2$.

Extra lemmas

theorem IMOSL.IMO2007N1.sq_mod_four_of_odd {m : ℕ} (hm : m % 2 = 1) : m ^ 2 % 4 = 1

theorem IMOSL.IMO2007N1.two_dvd_seven_pow_sub_three_pow (k n : ℕ) : 2 ∣ 7 ^ k - 3 ^ n

theorem IMOSL.IMO2007N1.succ_pow_four_lt_seven_mul_pow_four {a : ℕ} (ha : 2 ≤ a) : (a + 1) ^ 4 < 7 * a ^ 4

theorem IMOSL.IMO2007N1.succ_sq_lt_three_mul_sq {b : ℕ} (hb : 2 ≤ b) : (b + 1) ^ 2 < 3 * b ^ 2

theorem IMOSL.IMO2007N1.a_bound₀ {n k : ℕ} (hn : 2 ≤ n) (hk : 8 * n ^ 4 + k < 7 ^ n) (a : ℕ) : a ≥ n → 8 * a ^ 4 + k < 7 ^ a

theorem IMOSL.IMO2007N1.b_bound₀ {n k : ℕ} (hn : 2 ≤ n) (hk : 2 * n ^ 2 + k < 3 ^ n) (b : ℕ) : b ≥ n → 2 * b ^ 2 + k < 3 ^ b

theorem IMOSL.IMO2007N1.b_bound₁ (b : ℕ) : 2 * b ^ 2 < 3 ^ b

Start of the problem

def IMOSL.IMO2007N1.good (k n : ℕ) : Prop

Equations

• IMOSL.IMO2007N1.good k n = (7 ^ k - 3 ^ n ∣ ↑(k ^ 4 + n ^ 2))

theorem IMOSL.IMO2007N1.good_zero_zero : good 0 0

theorem IMOSL.IMO2007N1.good_two_four : good 2 4

theorem IMOSL.IMO2007N1.good_imp_even {k n : ℕ} (h : good k n) : 2 ∣ k ∧ 2 ∣ n

theorem IMOSL.IMO2007N1.good_two_mul_imp₁ {a b : ℕ} (h : good (2 * a) (2 * b)) : 7 ^ a + 3 ^ b ∣ 8 * a ^ 4 + 2 * b ^ 2

theorem IMOSL.IMO2007N1.good_two_mul_imp₂ {a b : ℕ} (h : 7 ^ a + 3 ^ b ∣ 8 * a ^ 4 + 2 * b ^ 2) : a = 0 ∧ b = 0 ∨ a = 1 ∧ b ≤ 2

theorem IMOSL.IMO2007N1.final_solution {k n : ℕ} : good k n ↔ k = 0 ∧ n = 0 ∨ k = 2 ∧ n = 4

Final solution