Compfiles/Usa2005P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2005, Problem 2

Prove that there do not exist integers x,y,z such that

x⁶ + x³ + x³y + y = 147¹⁵⁷ x³ + x³y + y² + y + z⁹ = 157¹⁴⁷.

Imports (2)
Imported by 1 file
  1. lemma Usa2005P2.lemma1 line 30 source

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

    Statement uses: ZMod, OfNat.ofNat, Nat, Or, Eq, HPow.hPow, Neg.neg

    Proof uses: Eq.mpr, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, id, Eq.trans, congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.IsInt.to_isNat, Tactic.ReduceModChar.CharP.isInt_of_mod, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Int, HMod.hMod, Mathlib.Meta.NormNum.isInt_emod, Mathlib.Meta.NormNum.IsInt.raw_refl, Mathlib.Meta.NormNum.isNat_natCast and 30 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. problem Usa2005P2.usa2005_p2 line 37 source

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

    Statement uses: Not, Exists, Int, And, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    Proof uses: Eq.mpr, Ne, id, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, ZMod, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.mp, congrArg, Eq.symm, Eq.refl, congrFun', Int.cast_add, congr, Int.cast_pow, Int.cast_mul, eq_of_heq and 109 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

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