# IMO 1981 Q3 #

Determine the maximum value of m ^ 2 + n ^ 2, where m and n are integers in {1, 2, ..., 1981} and (n ^ 2 - m * n - m ^ 2) ^ 2 = 1.

The trick to this problem is that m and n have to be consecutive Fibonacci numbers, because you can reduce any solution to a smaller one using the Fibonacci recurrence.

theorem Imo1981Q3.problemPredicate_iff (N : ) (m : ) (n : ) :
m Set.Ioc 0 N n Set.Ioc 0 N (n ^ 2 - m * n - m ^ 2) ^ 2 = 1
structure Imo1981Q3.ProblemPredicate (N : ) (m : ) (n : ) :
Instances For
theorem Imo1981Q3.ProblemPredicate.m_range {N : } {m : } {n : } (self : ) :
m Set.Ioc 0 N
theorem Imo1981Q3.ProblemPredicate.n_range {N : } {m : } {n : } (self : ) :
n Set.Ioc 0 N
theorem Imo1981Q3.ProblemPredicate.eq_one {N : } {m : } {n : } (self : ) :
(n ^ 2 - m * n - m ^ 2) ^ 2 = 1
Equations
Instances For
theorem Imo1981Q3.ProblemPredicate.m_le_n {N : } {m : } {n : } (h1 : ) :
m n
theorem Imo1981Q3.ProblemPredicate.eq_imp_1 {N : } {n : } (h1 : ) :
n = 1
theorem Imo1981Q3.ProblemPredicate.reduction {N : } {m : } {n : } (h1 : ) (h2 : 1 < n) :
def Imo1981Q3.NatPredicate (N : ) (m : ) (n : ) :
Equations
Instances For
theorem Imo1981Q3.NatPredicate.m_le_n {N : } {m : } {n : } (h1 : ) :
m n
theorem Imo1981Q3.NatPredicate.eq_imp_1 {N : } {n : } (h1 : ) :
n = 1
theorem Imo1981Q3.NatPredicate.reduction {N : } {m : } {n : } (h1 : ) (h2 : 1 < n) :
theorem Imo1981Q3.NatPredicate.n_pos {N : } {m : } {n : } (h1 : ) :
0 < n
theorem Imo1981Q3.NatPredicate.m_pos {N : } {m : } {n : } (h1 : ) :
0 < m
theorem Imo1981Q3.NatPredicate.n_le_N {N : } {m : } {n : } (h1 : ) :
n N
theorem Imo1981Q3.NatPredicate.imp_fib {N : } {n : } (m : ) :
∃ (k : ), m = k.fib n = (k + 1).fib
theorem Imo1981Q3.m_n_bounds {N : } {K : } (HK : N < K.fib + (K + 1).fib) {m : } {n : } (h1 : ) :
m K.fib n (K + 1).fib
theorem Imo1981Q3.k_bound {N : } {K : } (HK : N < K.fib + (K + 1).fib) {M : } (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) {m : } {n : } (h1 : ) :
m ^ 2 + n ^ 2 M
theorem Imo1981Q3.solution_bound {N : } {K : } (HK : N < K.fib + (K + 1).fib) {M : } (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) {k : } :
k M
theorem Imo1981Q3.solution_greatest {N : } {K : } (HK : N < K.fib + (K + 1).fib) {M : } (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) (H : Imo1981Q3.ProblemPredicate N K.fib (K + 1).fib) :
theorem imo1981_q3 :
IsGreatest () 3524578