Compfiles/Usa1985P1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1985, Problem 1

Determine whether or not there are any positive integral solutions of the simultaneous equations

x₁² + x₂² + ⋯ + x₁₉₈₅² = y³ x₁³ + x₂³ + ⋯ + x₁₉₈₅³ = z²

with distinct integers x₁, x₂, ⋯, x₁₉₈₅.

Imports (2)
Imported by 1 file
  1. lemma Usa1985P1.nicomachus line 33 source

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

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

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, zero_pow, Not, False, not_false_eq_true, eq_self, Eq.mpr, HAdd.hAdd, id, Finset.sum_range_succ, HMul.hMul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf and 47 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  2. lemma Usa1985P1.nicomachus' line 54 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, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun', Eq.symm, Nat.cast_one, Usa1985P1.nicomachus, Eq.mp, Finset.sum_range_succ', add_zero

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. determine Usa1985P1.does_exist line 64 source

    no axioms what this means

    Statement uses: Bool

    Proof uses: Bool.true

  4. abbrev Usa1985P1.is_valid line 66 source

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

    Statement uses: Nat, Int

    Proof uses: And, Membership.mem, Finset, Finset.range, OfNat.ofNat, LT.lt, Eq, Finset.sum, HPow.hPow, Ne

    10 instances, coercions and auxiliary constants left out.

  5. problem Usa1985P1.usa1985_p1 line 73 source

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

    Statement uses: ite, Eq, Bool, Usa1985P1.does_exist, Bool.true, Exists, Nat, Int, Usa1985P1.is_valid, Not

    Proof uses: Eq.mpr, id, Eq.trans, True, ite_congr, eq_self, Eq.refl, ite_true, Finset.sum, Finset.range, OfNat.ofNat, HAdd.hAdd, HPow.hPow, HMul.hMul, Membership.mem, Finset, LT.lt, Int.pos_of_sign_eq_one, rfl, Int.sign and 85 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 72 steps

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