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.m_range
{N : ℕ}
{m : ℤ}
{n : ℤ}
(self : Imo1981Q3.ProblemPredicate N m n)
:
theorem
Imo1981Q3.ProblemPredicate.n_range
{N : ℕ}
{m : ℤ}
{n : ℤ}
(self : Imo1981Q3.ProblemPredicate N m n)
:
theorem
Imo1981Q3.ProblemPredicate.m_le_n
{N : ℕ}
{m : ℤ}
{n : ℤ}
(h1 : Imo1981Q3.ProblemPredicate N m n)
:
m ≤ n
theorem
Imo1981Q3.ProblemPredicate.eq_imp_1
{N : ℕ}
{n : ℤ}
(h1 : Imo1981Q3.ProblemPredicate N n n)
:
n = 1
theorem
Imo1981Q3.ProblemPredicate.reduction
{N : ℕ}
{m : ℤ}
{n : ℤ}
(h1 : Imo1981Q3.ProblemPredicate N m n)
(h2 : 1 < n)
:
Imo1981Q3.ProblemPredicate N (n - m) m
Equations
- Imo1981Q3.NatPredicate N m n = Imo1981Q3.ProblemPredicate N ↑m ↑n
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)
:
Imo1981Q3.NatPredicate N (n - m) m
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