Compfiles/Imo1999P4.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1999, Problem 4

Determine all pairs of positive integers (n,p) such that p is a prime, n not exceeded 2p, and (p-1)ⁿ + 1 is divisible by of nᵖ⁻¹.

Imports (3)
Imported by 1 file
  1. lemma Imo1999P4.exists_least_prime_factor line 29 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Exists, And, Nat.Prime, Dvd.dvd, LE.le

    Proof uses: Exists.intro, Nat.minFac, And.intro, Nat.minFac_prime, Nat.minFac_dvd, Nat.minFac_le_of_dvd, Nat.Prime.two_le

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. lemma Imo1999P4.padicValNat_le_padicValNat_of_dvd line 35 source

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

    Statement uses: Nat, Ne, OfNat.ofNat, Nat.Prime, Dvd.dvd, LE.le, padicValNat

    Proof uses: Fact, Fact.mk, Eq.mpr, HPow.hPow, id, Eq, congrArg, Eq.symm, propext, padicValNat_dvd_iff_le, dvd_trans, pow_padicValNat_dvd

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. lemma Imo1999P4.aux₁ line 42 source

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

    Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Nat.Coprime, HSub.hSub, Dvd.dvd, HAdd.hAdd, HPow.hPow

    Proof uses: Fact, Fact.mk, And, orderOf, ZMod, HMul.hMul, Not, Eq.mpr, Eq, id, congr, congrArg, Or, Neg.neg, congrFun', Eq.trans, pow_mul', And.intro, Or.inr, eq_neg_of_add_eq_zero_left and 37 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  4. lemma Imo1999P4.aux₂ line 69 source

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

    Statement uses: Nat, Nat.Prime, Dvd.dvd, LE.le, Nat.Coprime, HSub.hSub, OfNat.ofNat

    Proof uses: Nat.coprime_of_dvd', False.elim, Nat.Prime.two_le, Nat.le_of_dvd

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  5. determine Imo1999P4.SolutionSet line 81 source

    standard axioms: propext what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Union.union, Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton, Set.ofPred, Imo1999P4.SolutionSet.match_1, And, Eq, Nat.Prime

    4 instances, coercions and auxiliary constants left out.

  6. problem Imo1999P4.imo1999_p4 line 83 source

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

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

    Proof uses: Iff.intro, Eq.mpr, Or, Eq, id, implies_congr, Union.union, Insert.insert, Singleton.singleton, Set.ofPred, Imo1999P4.SolutionSet.match_1, Eq.trans, congrFun', congrArg, congr, Prod.mk.injEq, Eq.refl, of_eq_true, True, eq_true and 137 more

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 137 steps

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