Compfiles/Imo1968P3.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1968, Problem 3

a, b, c are real with a non-zero. x1, x2, ... , xn satisfy the n equations:

a x_i^2 + b x_i + c = x_{i+1}, for 1 ≤ i < n

a x_n^2 + b x_n + c = x_1

Prove that the system has zero, 1 or >1 real solutions according as (b - 1)^2 - 4ac is <0, =0 or >0.

Imports (2)
Imported by 1 file
  1. def Imo1968P3.solution_set line 36 source

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

    Statement uses: Nat, Real, Set

    Proof uses: Set.ofPred, And, LT.lt, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, OfNat.ofNat, GT.gt

    13 instances, coercions and auxiliary constants left out.

  2. def Imo1968P3.f line 42 source

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

    Statement uses: Real

    Proof uses: HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, HSub.hSub

    13 instances, coercions and auxiliary constants left out.

  3. lemma Imo1968P3.f_continuous line 44 source

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

    Statement uses: Real, Continuous, Imo1968P3.f

    Proof uses: id, Continuous.add_const, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, HSub.hSub, Continuous.comp', Prod, Prod.mk, Prod.fst, Prod.snd, continuous_add, Continuous.prodMk, continuous_const_mul, Continuous.fun_pow, continuous_id'

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma Imo1968P3.IVT line 46 source

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

    Statement uses: Real, Continuous, LE.le, OfNat.ofNat, GE.ge, Exists, Eq

    Proof uses: Exists.imp, And, Membership.mem, Set, Set.uIcc, intermediate_value_uIcc, Continuous.continuousOn, Iff.mpr, Or, Set.mem_uIcc, Or.inl, And.intro

    42 instances, coercions and auxiliary constants left out.

  5. lemma Imo1968P3.sol_structure_f line 49 source

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

    Statement uses: Real, Ne, OfNat.ofNat, And, LT.lt, discrim, HSub.hSub, Not, Exists, Eq, Imo1968P3.f, Or, GE.ge, LE.le, GT.gt

    Proof uses: Iff, HAdd.hAdd, HMul.hMul, Iff.intro, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 162 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 51 steps

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

  6. lemma Imo1968P3.solution line 78 source

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

    Statement uses: Nat, Real, Eq, Imo1968P3.f, OfNat.ofNat, Membership.mem, Set, Imo1968P3.solution_set, ite, Finset, Finset.range, HAdd.hAdd

    Proof uses: id, Eq.mpr, And, LT.lt, HMul.hMul, HPow.hPow, congrFun', Set.ofPred, congrArg, GT.gt, funext, forall_congr, implies_congr, Eq.refl, And.intro, Eq.trans, Not, LE.le, ite_congr, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt and 74 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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

  7. lemma Imo1968P3.sum_sol line 100 source

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

    Statement uses: Nat, Real, Membership.mem, Set, Imo1968P3.solution_set, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, Imo1968P3.f

    Proof uses: id, HMul.hMul, HPow.hPow, HSub.hSub, Trans.trans, Finset.sum_congr, rfl, Finset, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.mpr, congrArg, Eq.symm and 50 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  8. problem Imo1968P3.imo1968_p3 line 115 source

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

    Statement uses: Nat, Real, Ne, OfNat.ofNat, And, LT.lt, discrim, HSub.hSub, Eq, Cardinal, Cardinal.mk, Imo1968P3.solution_set, GT.gt

    Proof uses: And.intro, Iff.mpr, Set, EmptyCollection.emptyCollection, Cardinal.mk_set_eq_zero_iff, Iff.mp, LE.le, Set.subset_empty_iff, Membership.mem, False.elim, Or, Imo1968P3.f, Classical.byContradiction, Not, Exists, False, Eq.mp, Eq.trans, congr, congrArg and 94 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 87 steps

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