Compfiles/Imo2005P4.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

4 declarations, 0 contain sorry, 0 declared as axioms

Intertional Mathematical Olympiad 2005, Problem 4

Determine all positive integers relatively prime to all the terms of the infinite sequence a n = 2 ^ n + 3 ^ n + 6 ^ n - 1, for n ≥ 1.

Imports (2)
Imported by 1 file
  1. def Imo2005P4.a line 29 source

    standard axioms: propext what this means

    Statement uses: Nat, Int

    Proof uses: HSub.hSub, HAdd.hAdd, HPow.hPow, OfNat.ofNat

    9 instances, coercions and auxiliary constants left out.

  2. theorem Imo2005P4.find_specified_factor Key lemma (a modular arithmetic calculation): Given a prime p other than 2 or 3, the (p - 2)th term of the sequence has p as a factor line 39 source

    Source documentation

    Key lemma (a modular arithmetic calculation): Given a prime p other than 2 or 3, the (p - 2)th term of the sequence has p as a factor.

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

    Statement uses: Nat, Nat.Prime, Ne, OfNat.ofNat, Dvd.dvd, Int, Imo2005P4.a, HSub.hSub

    Proof uses: Eq, Int.gcd, Iff.mpr, Nat.Coprime, HMul.hMul, And, Nat.coprime_mul_iff_right, And.intro, Eq.mp, Not, congrArg, Eq.symm, propext, Nat.Prime.coprime_iff_not_dvd, Nat.prime_dvd_prime_iff_eq, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true and 73 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) :
    ↑p ∣ a (p - 2) := by
…

    Mentions: Imo2005P4.a

  3. determine Imo2005P4.SolutionSet line 60 source

    standard axioms: propext what this means

    Statement uses: Set, PNat

    Proof uses: Singleton.singleton, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  4. problem Imo2005P4.imo2005_p4 line 62 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, LE.le, IsCoprime, Int, Imo2005P4.a, Membership.mem, PNat, Set, Imo2005P4.SolutionSet, Subtype.mk

    Proof uses: Subtype, Eq, Iff.intro, congrArg, Subtype.ext, Iff.trans, Nat.minFac, Decidable.byContradiction, Not, Nat.Prime, Nat.minFac_prime, Dvd.dvd, IsCoprime.of_isCoprime_of_dvd_right, Iff.mpr, Int.natCast_dvd_natCast, Nat.minFac_dvd, Eq.mp, propext, Prime.coprime_iff_not_dvd, Iff.mp and 25 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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