Compfiles/Imo1967P5.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1967, Problem 5

Consider the sequence {cₙ}, where

c₁ = a₁ + a₂ + ... + a₈ c₂ = a₁² + a₂² + ... + a₈² ... cₙ = a₁ⁿ + a₂ⁿ + ... + a₈ⁿ

in which a₁, a₂, ..., a₈ are real numbers not all equal to zero. Suppose that an infinite number of terms of the sequence {cₙ} are equal to zero. Find all natural numbers n such that cₙ = 0.

Imports (2)
Imported by 1 file
  1. determine Imo1967P5.solution line 38 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Set

    Proof uses: Set.ofPred, Odd

    3 instances, coercions and auxiliary constants left out.

  2. lemma Imo1967P5.odd_if_sum_eq_zero line 42 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, Real, Exists, And, Membership.mem, Ne, OfNat.ofNat, Eq, Finset.sum, HPow.hPow, Odd

    Proof uses: Decidable.byContradiction, Not, Even, Iff.mp, Nat.not_odd_iff_even, LT.lt, Trans.trans, LE.le, Even.pow_pos, Finset.single_le_sum, Even.pow_nonneg, False.elim, False, Eq.mp, Eq.trans, congrArg

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  3. lemma Imo1967P5.aux_recursive line 56 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Fin, OfNat.ofNat, Nat, Real, Set.Infinite, Set.ofPred, Eq, Finset.sum, HPow.hPow, Exists, And, Membership.mem, Ne, Odd

    Proof uses: PSigma.mk, PSigma

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 142 steps

    Open to load the checked before-and-after goal states.

  4. problem Imo1967P5.imo1967_p5 line 235 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Set.Infinite, Set.ofPred, Eq, Finset.sum, Finset.univ, HPow.hPow, Not, Set, Imo1967P5.solution

    Proof uses: Eq.mpr, Odd, id, congrArg, Imo1967P5.solution.eq_1, Set.ext, Finset, Exists, And, Membership.mem, Ne, of_eq_true, Eq.trans, True, funext, congrFun', true_and, eq_true, Eq.mp, Iff.intro and 2 more

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

    Open to load the checked before-and-after goal states.