Documentation

Archive.Imo.Imo1981Q3

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 : ) :
Imo1981Q3.ProblemPredicate 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 : Imo1981Q3.ProblemPredicate N m n) :
    m Set.Ioc 0 N
    theorem Imo1981Q3.ProblemPredicate.n_range {N : } {m : } {n : } (self : Imo1981Q3.ProblemPredicate N m n) :
    n Set.Ioc 0 N
    theorem Imo1981Q3.ProblemPredicate.eq_one {N : } {m : } {n : } (self : Imo1981Q3.ProblemPredicate N m n) :
    (n ^ 2 - m * n - m ^ 2) ^ 2 = 1
    Equations
    Instances For
      def Imo1981Q3.NatPredicate (N : ) (m : ) (n : ) :
      Equations
      Instances For
        theorem Imo1981Q3.NatPredicate.m_le_n {N : } {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) :
        m n
        theorem Imo1981Q3.NatPredicate.reduction {N : } {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) (h2 : 1 < n) :
        theorem Imo1981Q3.NatPredicate.n_pos {N : } {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) :
        0 < n
        theorem Imo1981Q3.NatPredicate.m_pos {N : } {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) :
        0 < m
        theorem Imo1981Q3.NatPredicate.n_le_N {N : } {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) :
        n N
        theorem Imo1981Q3.NatPredicate.imp_fib {N : } {n : } (m : ) :
        Imo1981Q3.NatPredicate N m n∃ (k : ), m = Nat.fib k n = Nat.fib (k + 1)
        theorem Imo1981Q3.m_n_bounds {N : } {K : } (HK : N < Nat.fib K + Nat.fib (K + 1)) {m : } {n : } (h1 : Imo1981Q3.NatPredicate N m n) :
        m Nat.fib K n Nat.fib (K + 1)
        theorem Imo1981Q3.k_bound {N : } {K : } (HK : N < Nat.fib K + Nat.fib (K + 1)) {M : } (HM : M = Nat.fib K ^ 2 + Nat.fib (K + 1) ^ 2) {m : } {n : } (h1 : Imo1981Q3.ProblemPredicate N m n) :
        m ^ 2 + n ^ 2 M
        theorem Imo1981Q3.solution_bound {N : } {K : } (HK : N < Nat.fib K + Nat.fib (K + 1)) {M : } (HM : M = Nat.fib K ^ 2 + Nat.fib (K + 1) ^ 2) {k : } :
        theorem Imo1981Q3.solution_greatest {N : } {K : } (HK : N < Nat.fib K + Nat.fib (K + 1)) {M : } (HM : M = Nat.fib K ^ 2 + Nat.fib (K + 1) ^ 2) (H : Imo1981Q3.ProblemPredicate N (Nat.fib K) (Nat.fib (K + 1))) :