Compfiles/Imo1967P3.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1967, Problem 3

Let $k, m, n$ be natural numbers such that m + k + 1 is a prime greater than n + 1. Let c(s) = s * (s+1). Prove that the product (c(m+1) - c(k)) * (c(m+2) - c(k)) * ... * (c(m+n) - c(k)) is divisible by the product c(1) * c(2) * ... * c(n).

Imports (2)
Imported by 1 file
  1. lemma Imo1967P3.aux_1 line 34 source

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

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

    Proof uses: Eq.mpr, id, congrArg, HPow.hPow, tsub_mul

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  2. lemma Imo1967P3.aux_1_mono line 43 source

    no axioms what this means

    Statement uses: Nat, Eq, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Monotone

    Proof uses: LE.le, Eq.mpr, id, congr, congrArg, Nat.mul_le_mul_right, Nat.mul_le_mul_left, Nat.succ_le_succ, LE.le.trans

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. lemma Imo1967P3.aux_2 line 53 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Nat.factorial, Finset.prod, Finset.Icc, HAdd.hAdd

    Proof uses: Eq, Nat.ascFactorial, Eq.mpr, Finset.range, id, congrArg, Nat.ascFactorial_eq_prod_range, Finset.Ico, Order.succ, Finset, Eq.symm, Finset.Ico_succ_right_eq_Icc, HSub.hSub, Finset.prod_Ico_eq_prod_range, Finset.prod_congr, rfl, Membership.mem, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul and 11 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  4. lemma Imo1967P3.aux_3 line 63 source

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

    Statement uses: Nat, And, LT.lt, OfNat.ofNat, Nat.Prime, HAdd.hAdd, Dvd.dvd, Nat.factorial, Finset.prod, Finset.Icc

    Proof uses: Imo1967P3.aux_2, HMul.hMul, Nat.zero_lt_succ, Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 68 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  5. lemma Imo1967P3.aux_4 line 92 source

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

    Statement uses: Nat, LE.le, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Eq, Finset.prod, Finset.Icc, Nat.descFactorial

    Proof uses: Eq.mpr, Finset.range, id, congrArg, Nat.descFactorial_eq_prod_range, Finset.Ico, Order.succ, Finset, Eq.symm, Finset.Ico_succ_right_eq_Icc, Finset.prod_Ico_eq_prod_range, Finset.prod_congr, rfl, Membership.mem

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  6. problem Imo1967P3.imo1967_p3 line 102 source

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

    Statement uses: Nat, And, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, Nat.Prime, Dvd.dvd, Int, Finset.prod, Finset.Icc, HSub.hSub

    Proof uses: Nat.factorial, Eq.mpr, id, Eq.trans, congr, congrArg, congrFun', Finset.prod_congr, Eq.refl, Finset, Membership.mem, Nat.le_induction, Nat.succ, of_eq_true, True, Singleton.singleton, zero_add, Finset.Icc_self, Finset.prod_singleton, one_mul and 75 more

    128 instances, coercions and auxiliary constants left out.

    Tactic trace: 96 steps

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