Compfiles/Imo1978P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1978, Problem 1

m and n are positive integers with m < n. The last three decimal digits of 1978ᵐ are the same as the last three decimal digits of 1978ⁿ. Find m and n such that m + n has the least possible value.

Imports (2)
Imported by 1 file
  1. determine Imo1978P1.solution line 28 source

    no axioms what this means

    Statement uses: Prod, Nat

    Proof uses: Prod.mk, OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  2. abbrev Imo1978P1.ValidPair line 30 source

    standard axioms: propext what this means

    Statement uses: Prod, Nat

    Proof uses: Imo1978P1.ValidPair.match_1, And, LE.le, OfNat.ofNat, LT.lt, Eq, HMod.hMod, HPow.hPow

    9 instances, coercions and auxiliary constants left out.

  3. problem Imo1978P1.imo1978_p1 line 33 source

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

    Statement uses: Nat, Eq, Prod, Prod.mk, Imo1978P1.solution, And, Imo1978P1.ValidPair, LE.le, HAdd.hAdd

    Proof uses: And.intro, Eq.mpr, id, congrArg, OfNat.ofNat, Imo1978P1.solution.eq_1, LT.lt, HMod.hMod, HPow.hPow, Imo1978P1.ValidPair.eq_1, of_eq_true, Eq.trans, True, congr, eq_true, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true and 144 more

    143 instances, coercions and auxiliary constants left out.

    Tactic trace: 116 steps

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