Compfiles/Imo1994P4.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1994, Problem 4

Determine all ordered pairs of positive integers (m, n) such that

(n³ + 1) / (mn - 1)

is an integer.

Imports (2)
Imported by 1 file
  1. lemma Imo1994P4.nonneg_mul_eq_two line 31 source

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

    Statement uses: Int, LE.le, OfNat.ofNat, Eq, HMul.hMul, Or, And

    Proof uses: LT.lt, Eq.mpr, id, congrArg, Eq.symm, Trans.trans, one_mul, Eq.refl, mul_le_mul, dite, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Not, HSub.hSub, Int.le_sub_one_of_not_le, Mathlib.Tactic.IntervalCases.of_le_left

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  2. lemma Imo1994P4.aux₁ line 41 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, Or, And

    Proof uses: HSub.hSub, Eq.mp, congrArg, one_mul, Imo1994P4.nonneg_mul_eq_two

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  3. lemma Imo1994P4.aux₂ line 52 source

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

    Statement uses: Int, LE.le, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd, Ne, False

    Proof uses: Eq.mpr, LT.lt, id, congrArg, Eq.symm, propext, lt_self_iff_false, Trans.trans, HSub.hSub, le_add_of_nonneg_right, sub_nonneg, one_mul, mul_le_mul, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 41 more

    87 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  4. determine Imo1994P4.SolutionSet line 74 source

    no axioms what this means

    Statement uses: Set, Prod, Int

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

    3 instances, coercions and auxiliary constants left out.

  5. problem Imo1994P4.imo1994_p4 line 79 source

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

    Statement uses: Int, Iff, Membership.mem, Prod, Set, Imo1994P4.SolutionSet, Prod.mk, And, LT.lt, OfNat.ofNat, Dvd.dvd, HSub.hSub, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat

    Proof uses: Iff.intro, Eq, Or, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congr, congrArg, Prod.mk.injEq, Eq.mpr, id, And.left, And.right, of_eq_true, True, eq_true, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 50 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 84 steps

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