Compfiles/Hungary1998P6.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Hungarian Mathematical Olympiad 1998, Problem 6

Let x, y, z be integers with z > 1. Show that

(x + 1)² + (x + 2)² + ... + (x + 99)² ≠ yᶻ.

Imports (3)
Imported by 1 file
  1. lemma Hungary1998P6.sum_range_square_mul_six line 30 source

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

    Statement uses: Nat, Eq, HMul.hMul, Finset.sum, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat

    Proof uses: Nat.recAux, Eq.refl, Eq.mpr, id, congrArg, Finset.sum_range_succ, add_mul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 22 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  2. lemma Hungary1998P6.sum_range_square line 38 source

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

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

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Hungary1998P6.sum_range_square_mul_six, Nat.mul_div_cancel, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  3. lemma Hungary1998P6.cast_sum_square line 43 source

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

    Statement uses: Nat, Eq, Int, Finset.sum, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat

    Proof uses: Eq.mpr, id, Eq.trans, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Eq.symm, Nat.cast_one

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. problem Hungary1998P6.hungary1998_p6 line 49 source

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

    Statement uses: Int, Nat, LT.lt, OfNat.ofNat, Ne, Finset.sum, Finset.range, HPow.hPow, HAdd.hAdd

    Proof uses: Eq, HMul.hMul, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, Finset.card, Finset.sum_const, Finset.card_range, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, eq_self, eq_true, True.intro, Eq.mpr, id and 75 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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