Compfiles/Imo1979P1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1979, Problem 1

Suppose that p and q are positive integers such that

p / q = 1 - 1/2 + 1/3 - 1/4 + ... - 1/1318 + 1/1319.

Prove that p is divisible by 1979.

Imports (2)
Imported by 1 file
  1. lemma Imo1979P1.lemma3 line 31 source

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

    Statement uses: Eq, Rat, Finset.sum, Nat, Finset.range, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Neg.neg, HAdd.hAdd, HSub.hSub, HMul.hMul

    Proof uses: Finset.filter, Even, Not, Finset.sum_filter_add_sum_filter_not, Eq.mpr, id, congrArg, Eq.symm, Function.Embedding, Function.Embedding.mk, Finset, Finset.map, Finset.ext, Iff, Membership.mem, Exists, And, propext, Finset.mem_map, Finset.mem_filter and 98 more

    142 instances, coercions and auxiliary constants left out.

    Tactic trace: 60 steps

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

  2. lemma Imo1979P1.lemma4 line 100 source

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

    Statement uses: Nat, Rat, Eq, Finset.sum, Finset.Ico, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Finset.range, HSub.hSub

    Proof uses: Eq.mpr, id, congrArg, Finset.sum_Ico_eq_sum_range, add_tsub_cancel_left, two_mul, Finset.sum_range_add, Finset.sum_add_distrib, HAdd, Eq.rec, Eq.refl, Eq.symm, Finset.sum_range_reflect, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.mp, LT.lt, propext and 1 more

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  3. lemma Imo1979P1.lemma9' line 111 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.range, OfNat.ofNat, Eq, Rat, HDiv.hDiv, Finset.prod, HMul.hMul, HAdd.hAdd, HSub.hSub, Finset.erase

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Finset.prod_erase_mul, LE.le, Eq.mp, LT.lt, propext, Finset.mem_range, congr, congrFun', Eq.trans, Nat.cast_mul, Finset.prod_natCast, Finset.prod_congr, Eq.refl, Nat.cast_add, Nat.cast_sub, Rat.mul_div_cancel and 68 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  4. lemma Imo1979P1.lemma9 line 123 source

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

    Statement uses: Eq, Rat, HMul.hMul, Finset.sum, Nat, Finset.range, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, HSub.hSub, Finset.prod, Finset.erase

    Proof uses: Eq.mpr, id, congrFun', congrArg, Finset.sum_mul, Finset.sum_congr, Eq.refl, Finset, Membership.mem, div_mul_eq_mul_div, one_mul, rfl, Imo1979P1.lemma9', congr, Eq.trans, Finset.prod_natCast, Finset.prod_congr, Nat.cast_mul, Nat.cast_add, Nat.cast_sum

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  5. lemma Imo1979P1.h4 line 133 source

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

    Statement uses: Nat, Membership.mem, Finset, Finset.range, OfNat.ofNat, Eq, Rat, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HMul.hMul

    Proof uses: Eq.mpr, id, congrFun', congrArg, Nat.cast_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_pf_add_overlap, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_add and 91 more

    130 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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

  6. lemma Imo1979P1.prime_1979 line 155 source

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

    Statement uses: Nat.Prime, OfNat.ofNat, Nat

    Proof uses: Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_3, Bool.false, Mathlib.Meta.NormNum.minFacHelper_2, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Mathlib.Meta.NormNum.minFacHelper_0

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. problem Imo1979P1.imo1979_p1 line 159 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Eq, Rat, HDiv.hDiv, Finset.sum, Nat, Finset.range, HPow.hPow, Neg.neg, HAdd.hAdd, Dvd.dvd

    Proof uses: HMul.hMul, HSub.hSub, Trans.trans, Finset.Ico, rfl, Imo1979P1.lemma3, Eq.mpr, id, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.symm, Finset.mul_sum, Rat.mul_assoc, mul_one_div_cancel, of_decide_eq_true, Ne and 66 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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