Compfiles/Imo1981P4.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1981, Problem 4

(a) For which values of $n>2$ is there a set of $n$ consecutive positive integers such that the largest number in the set is a divisor of the least common multiple of the remaining $n-1$ numbers?

(b) For which values of $n>2$ is there exactly one set having the stated property?

Imports (2)
Imported by 1 file
  1. def Imo1981P4.last_divides_lcm_remaining line 31 source

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

    Statement uses: Nat

    Proof uses: Dvd.dvd, HAdd.hAdd, Finset.lcm, Finset.Icc, OfNat.ofNat, HSub.hSub, id

    11 instances, coercions and auxiliary constants left out.

  2. theorem Imo1981P4.not_existsUnique_of_not_exists line 35 source

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

    Statement uses: Not, Exists, ExistsUnique

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Imo1981P4.not_existsUnique_of_exists_ne line 38 source

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

    Statement uses: Ne, Not, ExistsUnique

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Imo1981P4.dvd_factorial line 42 source

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

    Statement uses: Nat, Imo1981P4.last_divides_lcm_remaining, Dvd.dvd, HAdd.hAdd, Nat.factorial, HSub.hSub, OfNat.ofNat

    Proof uses: Finset.prod, Finset.Icc, id, dvd_trans, Finset.lcm, Finset.lcm_dvd_prod, Eq.mpr, Finset.range, Eq, congrArg, Nat.factorial_eq_prod_range_add_one, Eq.mp, Int, Eq.trans, Finset.prod_congr, Eq.refl, Finset, Membership.mem, Eq.symm, Nat.cast_one and 33 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

  5. theorem Imo1981P4.not_3 line 66 source

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

    Statement uses: Not, Exists, Nat, Imo1981P4.last_divides_lcm_remaining, OfNat.ofNat

    Proof uses: id, False, Dvd.dvd, HAdd.hAdd, Nat.factorial, HSub.hSub, Imo1981P4.dvd_factorial, LE.le, Nat.le_of_dvd, of_eq_true, LT.lt, Eq.trans, True, Eq.mp, congrArg, Eq, Eq.refl

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  6. theorem Imo1981P4.unique_4 line 75 source

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

    Statement uses: ExistsUnique, Nat, Imo1981P4.last_divides_lcm_remaining, OfNat.ofNat

    Proof uses: Exists.intro, And, Eq, And.intro, id, of_decide_eq_true, Dvd.dvd, HAdd.hAdd, Finset.lcm, Finset.Icc, HSub.hSub, Bool, Decidable.decide, Bool.true, Eq.refl, Classical.byContradiction, Not, Exists, Ne, False and 11 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  7. theorem Imo1981P4.coprime_sub_succ line 91 source

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

    Statement uses: Nat, LT.lt, Nat.Coprime, HSub.hSub, HAdd.hAdd, OfNat.ofNat

    Proof uses: Eq.mpr, id, Eq, congrArg, Nat.succ, Nat.sub_succ', propext, Nat.coprime_self_sub_right, of_eq_true, Nat.coprime_one_right_eq_true

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  8. theorem Imo1981P4.lcm_sub_succ line 96 source

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

    Statement uses: Nat, LT.lt, Eq, Nat.lcm, HSub.hSub, HAdd.hAdd, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.Coprime.lcm_eq_mul, Imo1981P4.coprime_sub_succ

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  9. theorem Imo1981P4.ge_5 line 100 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Or, Eq, Imo1981P4.last_divides_lcm_remaining, HSub.hSub, Nat.lcm, HAdd.hAdd

    Proof uses: Eq.mpr, HMul.hMul, id, congrArg, Imo1981P4.lcm_sub_succ, Dvd.dvd, Finset.lcm, Finset.Icc, Nat.sub_add_cancel, Int, Eq.trans, Nat.cast_mul, Nat.cast_sub, sub_mul, mul_sub, Eq.symm, propext, sub_nonneg, Or.elim, congrFun' and 89 more

    143 instances, coercions and auxiliary constants left out.

    Tactic trace: 57 steps

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

  10. determine Imo1981P4.values_a line 138 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.Ici, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  11. determine Imo1981P4.values_b line 140 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Singleton.singleton, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  12. problem Imo1981P4.imo1981_p4 line 142 source

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

    Statement uses: Nat, And, Iff, Membership.mem, Set, Imo1981P4.values_a, LT.lt, OfNat.ofNat, Exists, Imo1981P4.last_divides_lcm_remaining, Imo1981P4.values_b, ExistsUnique

    Proof uses: And.intro, id, Iff.intro, Set.Ici, Or, Eq, LE.le, Or.elim, ExistsUnique.exists, Imo1981P4.unique_4, Eq.symm, Exists.intro, HSub.hSub, Nat.lcm, HAdd.hAdd, Imo1981P4.ge_5, of_eq_true, Eq.trans, True, False and 99 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

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