Compfiles/Usa2003P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2003, Problem 1

Prove that for every positive integer n there exists an n-digit number divisible by 5ⁿ, all of whose digits are odd.

Imports (3)
Imported by 1 file
  1. lemma Usa2003P1.nat_mod_inv line 30 source

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

    Statement uses: Nat, Exists, Eq, HMod.hMod, HAdd.hAdd, OfNat.ofNat

    Proof uses: Exists.intro, HSub.hSub

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Usa2003P1.lemma2 line 32 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Coprime, Exists, And, Nat.ModEq, HMul.hMul

    Proof uses: Subtype, Nat.chineseRemainder, Dvd.dvd, Iff.mp, Nat.modEq_zero_iff_dvd, Eq, Exists.intro, HMod.hMod, And.intro, Nat.mod_lt, id, Eq.mpr, congrArg, Eq.symm, Nat.mul_mod, Nat.mod_mod, Eq.refl

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  3. problem Usa2003P1.usa2003_p1 line 44 source

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

    Statement uses: Nat, Exists, And, Eq, List.length, Nat.digits, OfNat.ofNat, Dvd.dvd, HPow.hPow, Bool, List.all, Decidable.decide, Odd, Bool.true

    Proof uses: Nat.recAux, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', List, List.nil, Nat.digits_zero, eq_self, pow_zero, IsUnit, Units, and_self, HAdd.hAdd, HMul.hMul, LT.lt, HMod.hMod and 67 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 45 steps

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