Compfiles/Imo1979P5.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1979, Problem 5

Find all real numbers a for which there exist non-negative real numbers x1, x2, x3, x4, x5 satisfying:

x1 + 2x_2 + 3x_3 + 4x_4 + 5x_5 = a, x1 + 2^3x_2 + 3^3x_3 + 4^3x_4 + 5^3x_5 = a^2, x1 + 2^5x_2 + 3^5x_3 + 4^5x_4 + 5^5x_5 = a^3.

Imports (2)
Imported by 1 file
  1. determine Imo1979P5.solution_set line 30 source

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

    Statement uses: Set, Real

    Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton

    12 instances, coercions and auxiliary constants left out.

  2. problem Imo1979P5.imo1979_p5 line 32 source

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

    Statement uses: Real, Iff, Exists, And, GE.ge, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, Nat, HPow.hPow, Membership.mem, Set, Imo1979P5.solution_set

    Proof uses: Iff.intro, HSub.hSub, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Mathlib.Tactic.LinearCombination.mul_const_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 100 more

    124 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

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