Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1999P3

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.RingTheory.RootsOfUnity.Complex
public import Mathlib.RingTheory.SimpleRing.Principal

public section


/-!
# USA Mathematical Olympiad 1999, Problem 3

Let p > 2 be a prime and let a, b, c, d be integers not divisible by p, such that

    {ra/p} + {rb/p} + {rc/p} + {rd/p} = 2

for any integer r not divisible by p. (Here, {t} = t − ⌊t⌋ is the fractional part.)
Prove that at least two of the numbers a + b, a + c, a + d, b + c, b + d, c + d
are divisible by p.
-/

namespace Usa1999P3

open Finset

theorem usa1999_p3 (p : ℕ) (hp : p.Prime) (hp2 : 2 < p) (a b c d : ℤ)
    (ha : ¬ (p : ℤ) ∣ a) (hb : ¬ (p : ℤ) ∣ b) (hc : ¬ (p : ℤ) ∣ c) (hd : ¬ (p : ℤ) ∣ d)
    (h : ∀ n : ℤ, ¬ (p : ℤ) ∣ n →
      Int.fract (((n * a : ℤ) : ℝ) / (p : ℝ)) + Int.fract (((n * b : ℤ) : ℝ) / (p : ℝ)) +
      Int.fract (((n * c : ℤ) : ℝ) / (p : ℝ)) + Int.fract (((n * d : ℤ) : ℝ) / (p : ℝ)) = 2) :
    (p : ℤ) ∣ a + b ∧ (p : ℤ) ∣ c + d ∨
      (p : ℤ) ∣ a + c ∧ (p : ℤ) ∣ b + d ∨
        (p : ℤ) ∣ a + d ∧ (p : ℤ) ∣ b + c := sorry

end Usa1999P3

File author(s): Kimi K3

This problem has a complete formalized solution.