Compfiles/Imo2002P3.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2002, Problem 3

Find all pairs of positive integers m,n ≥ 3 for which there exist infinitely many positive integers a such that

(aᵐ + a - 1) / (aⁿ + a² - 1)

is itself an integer.

Imports (2)
Imported by 1 file
  1. lemma Imo2002P3.natDegree_numerpol line 40 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Polynomial.natDegree, Int, HSub.hSub, Polynomial, HAdd.hAdd, HPow.hPow, Polynomial.X

    Proof uses: Mathlib.Tactic.ComputeDegree.natDegree_eq_of_le_of_coeff_ne_zero', Max.max, HMul.hMul, ite, Polynomial.natDegree_sub_le_of_le, Polynomial.natDegree_add_le_of_le, Polynomial.natDegree_pow_le_of_le, Polynomial.natDegree_X_le, Mathlib.Tactic.ComputeDegree.natDegree_one_le, Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq, Mathlib.Tactic.ComputeDegree.coeff_add_of_eq, Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite', Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, mul_one, le_refl, Mathlib.Tactic.ComputeDegree.coeff_congr_lhs and 26 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. lemma Imo2002P3.monic_numerpol line 44 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial.Monic, Int, HSub.hSub, Polynomial, HAdd.hAdd, HPow.hPow, Polynomial.X

    Proof uses: Polynomial.Monic.sub_of_left, Polynomial.monic_X_pow_add, Eq.mpr, LT.lt, WithBot, Polynomial.degree, id, Eq, congrArg, Polynomial.degree_X, propext, Nat.one_lt_cast, Polynomial.degree_one, Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_X_pow, AddUnits

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  3. lemma Imo2002P3.natDegree_denompol line 56 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Polynomial.natDegree, Int, HSub.hSub, Polynomial, HAdd.hAdd, HPow.hPow, Polynomial.X

    Proof uses: Mathlib.Tactic.ComputeDegree.natDegree_eq_of_le_of_coeff_ne_zero', Max.max, HMul.hMul, ite, Polynomial.natDegree_sub_le_of_le, Polynomial.natDegree_add_le_of_le, Polynomial.natDegree_pow_le_of_le, Polynomial.natDegree_X_le, Mathlib.Tactic.ComputeDegree.natDegree_one_le, Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq, Mathlib.Tactic.ComputeDegree.coeff_add_of_eq, Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite', Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, mul_one, le_refl, Mathlib.Tactic.ComputeDegree.coeff_congr_lhs and 27 more

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. lemma Imo2002P3.monic_denompol line 60 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Polynomial.Monic, Int, HSub.hSub, Polynomial, HAdd.hAdd, HPow.hPow, Polynomial.X

    Proof uses: Polynomial.Monic.sub_of_left, Polynomial.monic_X_pow_add, Eq.mpr, LT.lt, WithBot, Polynomial.degree, id, Eq, congrArg, Polynomial.degree_X_pow, propext, Nat.cast_lt, Polynomial.degree_one, Polynomial.degree_add_eq_left_of_degree_lt, congr, AddUnits

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  5. lemma Imo2002P3.proof_body line 72 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Set.Infinite, Int, Set.ofPred, And, LT.lt, Dvd.dvd, HSub.hSub, HAdd.hAdd, HPow.hPow, Eq

    Proof uses: Polynomial, Polynomial.X, Polynomial.dvd_of_infinite_eval_dvd_eval, Imo2002P3.monic_denompol, Set.Infinite.mono, Polynomial.eval, of_eq_true, Set, Eq.trans, True, congrArg, funext, congr, Polynomial.eval_sub, Polynomial.eval_add, Polynomial.eval_pow, congrFun', Polynomial.eval_X, Polynomial.eval_one, forall_congr and 169 more

    256 instances, coercions and auxiliary constants left out.

    Tactic trace: 45 steps

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

  6. determine Imo2002P3.solution line 117 source

    no axioms what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Singleton.singleton, Prod.mk, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  7. problem Imo2002P3.imo2002_p3 line 119 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Iff, Membership.mem, Prod, Set, Imo2002P3.solution, Prod.mk, Set.Infinite, Int, Set.ofPred, And, LT.lt, Dvd.dvd, HSub.hSub, HAdd.hAdd, HPow.hPow

    Proof uses: Eq.mpr, Eq, id, congrFun', congrArg, Eq.trans, Singleton.singleton, Prod.mk.injEq, Iff.intro, And.left, And.right, HMul.hMul, Eq.rec, Eq.refl, funext, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat and 51 more

    67 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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