Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2009P6

module

public import Mathlib.Algebra.GCDMonoid.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Analysis.Normed.Field.Lemmas
public import Mathlib.Data.Int.Star
public import Mathlib.NumberTheory.Padics.PadicVal.Basic
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas

public section


/-!
# USA Mathematical Olympiad 2009, Problem 6

Let $s_1, s_2, s_3, \ldots$ be an infinite, nonconstant sequence of rational numbers, meaning it
is not the case that $s_1 = s_2 = s_3 = \ldots$. Suppose that $t_1, t_2, t_3, \ldots$ is also an
infinite, nonconstant sequence of rational numbers with the property that $(s_i - s_j)(t_i - t_j)$
is an integer for all $i$ and $j$. Prove that there exists a rational number $r$ such that
$(s_i - s_j) r$ and $(t_i - t_j)/r$ are integers for all $i$ and $j$.
-/

namespace Usa2009P6

theorem usa2009_p6 (s t : ℕ → ℚ) (hs : ¬ ∀ i j, s i = s j) (ht : ¬ ∀ i j, t i = t j)
    (h : ∀ i j, ∃ k : ℤ, (s i - s j) * (t i - t j) = k) :
    ∃ r : ℚ, r ≠ 0 ∧ (∀ i j, ∃ k : ℤ, (s i - s j) * r = k) ∧
      ∀ i j, ∃ k : ℤ, (t i - t j) / r = k := sorry

end Usa2009P6

File author(s): Kimi K3

This problem has a complete formalized solution.