Compfiles/Imo1990P3.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1990, Problem 3

Find all integers n > 1 such that n² divides 2ⁿ + 1.

Imports (3)
Imported by 1 file
  1. determine Imo1990P3.solution_set line 26 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Singleton.singleton, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  2. lemma Imo1990P3.aux_1 line 30 source

    standard axioms: propext what this means

    Statement uses: Nat, Or, Nat.ModEq, OfNat.ofNat, HPow.hPow

    Proof uses: LT.lt, HMod.hMod, Nat.mod_lt, Nat.zero_lt_succ, Eq.mpr, HAdd.hAdd, HMul.hMul, HDiv.hDiv, id, Eq, congrArg, Eq.symm, Nat.div_add_mod, dite, LE.le, Or.inr, Nat.recAux, Iff.mp, Dvd.dvd, Int and 40 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

  3. lemma Imo1990P3.imo_1990_p3_forward line 60 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, Eq

    Proof uses: dite, LT.lt, False.elim, False, Eq.mp, Nat.dvd_eq_false_of_mod_ne_zero, eagerReduce, Bool, Bool.true, Eq.refl, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.IntervalCases.of_le_left, Not, Odd and 247 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 398 steps (first 200 of 398)

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

  4. problem Imo1990P3.imo1990_p3 line 408 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Imo1990P3.solution_set, Dvd.dvd, HPow.hPow, HAdd.hAdd

    Proof uses: Iff.intro, Eq.mpr, id, Eq, congrArg, Eq.mp, Singleton.singleton, propext, Set.mem_singleton_iff, Mathlib.Meta.NormNum.isNat_dvd_true, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.IsNatPowT.bit1, Imo1990P3.imo_1990_p3_forward

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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