Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2004P2

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.GCDMonoid.Finset
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.NormNum.DivMod
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2004, Problem 2

Suppose a₁, a₂, …, aₙ are integers whose greatest common divisor is 1.
Let S be a set of integers with the following properties:

(a) For i = 1, 2, …, n, aᵢ ∈ S.

(b) For i, j = 1, 2, …, n (not necessarily distinct), aᵢ − aⱼ ∈ S.

(c) For any integers x, y ∈ S, if x + y ∈ S, then x − y ∈ S.

Prove that S must equal the set of all integers.
-/

namespace Usa2004P2

theorem usa2004_p2 {n : ℕ} (a : Fin n → ℤ) (S : Set ℤ)
    (hgcd : Finset.univ.gcd a = 1)
    (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S) :
    S = Set.univ := sorry

end Usa2004P2

File author(s): Kimi K3

This problem has a complete formalized solution.