Compfiles/Imo1989P5.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1989, Problem 5

Prove that for each positive integer n there exist n consecutive positive integers, none of which is an integral power of a prime number.

Imports (5)
Imported by 1 file
  1. structure Imo1989P5.ChinesePair line 31 source

    no axioms what this means

  2. lemma Imo1989P5.general_chinese_remainder line 35 source

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

    Statement uses: List, Imo1989P5.ChinesePair, List.Pairwise, Nat.Coprime, Imo1989P5.ChinesePair.modulus, Exists, Nat, Membership.mem, Nat.ModEq, Imo1989P5.ChinesePair.remainder

    Proof uses: List.rec, List.nil, Exists.intro, OfNat.ofNat, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, List.cons, List.Pairwise.tail, List.prod, List.map, Iff.mpr, Nat.coprime_list_prod_right_iff, And, Eq.mp, congrArg and 14 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  3. lemma Imo1989P5.list_upper_bound line 59 source

    standard axioms: propext what this means

    Statement uses: List, Nat, Exists, Membership.mem, LE.le

    Proof uses: Exists.intro, List.foldr, Max.max, Bot.bot, List.le_max_of_le, le_refl

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  4. theorem Imo1989P5.get_primes line 64 source

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

    Statement uses: Nat, Exists, List, And, Eq, List.length, List.Nodup, Membership.mem, Nat.Prime, LE.le

    Proof uses: Nat.recAux, Exists.intro, OfNat.ofNat, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, List.nil, forall_congr, False, implies_congr, Eq.refl, implies_true, and_self, HAdd.hAdd, Imo1989P5.list_upper_bound, Max.max and 16 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  5. lemma Imo1989P5.not_prime_power_of_two_factors line 84 source

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

    Statement uses: Nat, Nat.Prime, Ne, Dvd.dvd, Not, IsPrimePow

    Proof uses: OfNat.ofNat, IsPrimePow.ne_zero, Exists, And, Prime, LT.lt, Eq, HPow.hPow, False, Membership.mem, List, Nat.primeFactorsList, Iff.mpr, Nat.mem_primeFactorsList, Eq.mp, congrArg, Eq.symm, And.intro, And.right, Iff.mp and 6 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  6. lemma Imo1989P5.lemma1 line 103 source

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

    Statement uses: Nat, Nat.Prime, Ne, Nat.Coprime, HMul.hMul

    Proof uses: Iff.mpr, Nat.coprime_primes, Nat.Coprime.mul_left

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  7. lemma Imo1989P5.lemma2 line 114 source

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

    Statement uses: Nat, Nat.Prime, Ne, Nat.Coprime, HMul.hMul

    Proof uses: Imo1989P5.lemma1, Nat.Coprime.mul_right

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  8. lemma Imo1989P5.lemma3 line 128 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: List, List.Nodup, Fin, List.length, Ne, List.get

    Proof uses: Eq, Iff.mp, Function.Injective, List.nodup_iff_injective_get

    Tactic trace: 2 steps

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

  9. problem Imo1989P5.imo1989_p5 line 139 source

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

    Statement uses: Nat, Exists, LT.lt, Not, IsPrimePow, HAdd.hAdd

    Proof uses: List, And, Eq, List.length, HMul.hMul, OfNat.ofNat, List.Nodup, Membership.mem, Nat.Prime, LE.le, Imo1989P5.get_primes, Imo1989P5.ChinesePair, List.ofFn, Fin, List.get, Fin.mk, Imo1989P5.ChinesePair.mk, HSub.hSub, List.Pairwise, Nat.Coprime and 53 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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