IMO 2018 N5

Determine whether there exists $x, y, z, t ∈ ℕ^+$ such that $xy - zt = x + y = z + t$ and both $xy$ and $zt$ are perfect squares.

Extra lemmas

theorem IMOSL.IMO2018N5.even_mul_of_odd_add {x y : ℤ} (h : Odd (x + y)) : Even (x * y)

theorem IMOSL.IMO2018N5.sq_sub_eq_sq_bound {a b : ℤ} (hb : 0 < b) (h : ∃ (c : ℤ), a ^ 2 - b = c ^ 2) : 2 * a - 1 ≤ b

General theory of good quadruplet

def IMOSL.IMO2018N5.good (v : Fin 4 → ℤ) : Prop

Equations

• IMOSL.IMO2018N5.good v = (v 0 * v 1 - v 2 * v 3 = v 0 + v 1 ∧ v 0 + v 1 = v 2 + v 3)

def IMOSL.IMO2018N5.mkGood (k l : ℤ) : Fin 4 → ℤ

Equations

• IMOSL.IMO2018N5.mkGood k l = ![2 * (k * l) + (k - l), 2 * (k * l) - (k - l), 2 * (k * l) + (k + l), 2 * (k * l) - (k + l)]

def IMOSL.IMO2018N5.mkGood_good (k l : ℤ) : good (mkGood k l)

Equations

• ⋯ = ⋯

theorem IMOSL.IMO2018N5.good.eq_mkGood {v : Fin 4 → ℤ} (hv : good v) : ∃ (k : ℤ), ∃ (l : ℤ), v = mkGood k l

theorem IMOSL.IMO2018N5.good_iff_eq_mkGood {v : Fin 4 → ℤ} : good v ↔ ∃ (k : ℤ), ∃ (l : ℤ), v = mkGood k l

theorem IMOSL.IMO2018N5.mkGood_prod (k l : ℤ) : mkGood k l 0 * mkGood k l 1 * (mkGood k l 2 * mkGood k l 3) = ((2 * (k * l)) ^ 2 - (k ^ 2 + l ^ 2)) ^ 2 - (2 * (k * l)) ^ 2

theorem IMOSL.IMO2018N5.good.prod_eq_sq_imp' {v : Fin 4 → ℤ} (hv : good v) (h : ∃ (a : ℤ), v 0 * v 1 * (v 2 * v 3) = a ^ 2) : (∃ (x : ℤ), ∃ (z : ℤ), v = ![x, -x, z, -z]) ∨ (v = ![2, 2, 4, 0] ∨ v = ![0, -4, -2, -2]) ∨ v = ![-4, 0, -2, -2] ∨ v = ![2, 2, 0, 4]

theorem IMOSL.IMO2018N5.good.prod_eq_sq_imp {v : Fin 4 → ℤ} (hv : good v) (h : ∃ (a : ℤ), v 0 * v 1 = a ^ 2) (h0 : ∃ (b : ℤ), v 2 * v 3 = b ^ 2) : v = ![0, 0, 0, 0] ∨ (v = ![2, 2, 4, 0] ∨ v = ![0, -4, -2, -2]) ∨ v = ![-4, 0, -2, -2] ∨ v = ![2, 2, 0, 4]

theorem IMOSL.IMO2018N5.final_solution {v : Fin 4 → ℤ} (hv : good v) (hv0 : ∀ (i : Fin 4), v i ≠ 0) : ¬((∃ (x : ℤ), v 0 * v 1 = x ^ 2) ∧ ∃ (y : ℤ), v 2 * v 3 = y ^ 2)

Final solution