Compfiles/Imo2018P2.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2018, Problem 2

Determine all integers n ≥ 3 such that there exist real numbers a₁, a₂, ..., aₙ satisfying

aᵢaᵢ₊₁ + 1 = aᵢ₊₂,

where the indices are taken mod n.

Imports (2)
Imported by 1 file
  1. abbrev Imo2018P2.P line 30 source

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

    Statement uses: Nat, ZMod, Real

    Proof uses: Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    18 instances, coercions and auxiliary constants left out.

  2. lemma Imo2018P2.not_dvd_prime_exists_mod_inverse line 35 source

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

    Statement uses: Nat, NeZero, Nat.Prime, LT.lt, OfNat.ofNat, Not, Dvd.dvd, Exists, ZMod, Eq, HMul.hMul

    Proof uses: And, HMod.hMod, Nat.exists_mul_mod_eq_one_of_coprime, Iff.mpr, Nat.Coprime, Nat.Prime.coprime_iff_not_dvd, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, Nat.cast_one, Nat.cast_mul, Nat.ModEq, propext, ZMod.natCast_eq_natCast_iff, Nat.mod_eq_of_lt, And.right

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  3. lemma Imo2018P2.mod_3_satisfies line 46 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, Exists, ZMod, Real, Imo2018P2.P

    Proof uses: Fact, LT.lt, Fact.mk, Nat.lt_of_add_left_lt, ite, ZMod.val, Neg.neg, Exists.intro, Or, And, Not, HAdd.hAdd, Mathlib.Tactic.ModCases.NatMod.onModCases_start, Eq.refl, Bool, Bool.true, Mathlib.Tactic.ModCases.NatMod.onModCases_succ, Nat.ModEq, Eq.mpr, Eq and 54 more

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  4. lemma Imo2018P2.three_periodic line 74 source

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

    Statement uses: Nat, NeZero, ZMod, Real, Imo2018P2.P, Eq, HAdd.hAdd, OfNat.ofNat

    Proof uses: HSub.hSub, HPow.hPow, HMul.hMul, Trans.trans, Eq.mpr, id, congrArg, Eq.symm, of_eq_true, Eq.trans, True, congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr and 96 more

    137 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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

  5. lemma Imo2018P2.satisfies_is_mod_3 line 127 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, ZMod, Real, Imo2018P2.P, Dvd.dvd

    Proof uses: LT.lt, Nat.lt_of_add_left_lt, Fact, Fact.mk, Eq, HAdd.hAdd, HMul.hMul, Eq.mpr, ZMod.val, id, congrArg, Eq.symm, ZMod.natCast_zmod_val, Nat.recAux, of_eq_true, Eq.trans, True, congrFun', Nat.cast_zero, MulZeroClass.mul_zero and 191 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 36 steps

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

  6. determine Imo2018P2.solution_set line 172 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, Dvd.dvd

    3 instances, coercions and auxiliary constants left out.

  7. problem Imo2018P2.imo2018_p2 line 174 source

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

    Statement uses: Nat, Iff, Membership.mem, Set, Imo2018P2.solution_set, And, LE.le, OfNat.ofNat, Exists, ZMod, Real, Imo2018P2.P

    Proof uses: Iff.intro, Dvd.dvd, And.intro, Imo2018P2.mod_3_satisfies, Imo2018P2.satisfies_is_mod_3

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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