Compfiles/Usa1988P1.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

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1988, Problem 1

The repeating decimal 0.ab ... k pq ... u = m/n, where m and n are relatively prime integers, and there is at least one decimal before the repeating part. Show that n is divisible by 2 or 5 (or both). [For example, 0.01136̅ = 0.01136363636 ... = 1/88 and 88 is divisible by 2.]

Imports (6)
Imported by 1 file
  1. lemma Usa1988P1.not_ten_dvd_num The numerator a * (10 ^ s - 1) + b of the unreduced fraction is congruent to b - a modulo 10, so it is not divisible by 10 when the last digits of a and b differ line 52 source

    Source documentation

    The numerator a * (10 ^ s - 1) + b of the unreduced fraction is congruent to b - a modulo 10, so it is not divisible by 10 when the last digits of a and b differ.

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Ne, HMod.hMod, Not, Dvd.dvd, HAdd.hAdd, HMul.hMul, HSub.hSub, HPow.hPow

    Proof uses: Nat.ModEq, Iff.mpr, Nat.modEq_zero_iff_dvd, dvd_mul_of_dvd_right, dvd_pow_self, Iff.mp, Nat.one_le_iff_ne_zero, Eq, Eq.mpr, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Nat.sub_add_cancel, Nat.one_le_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool and 10 more

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

    lemma not_ten_dvd_num {a b s : ℕ} (hs : 1 ≤ s) (hab : a % 10 ≠ b % 10) :
    ¬ 10 ∣ a * (10 ^ s - 1) + b := by
…
  2. problem Usa1988P1.usa1988_p1 line 71 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Ne, HMod.hMod, Nat.Coprime, Eq, Rat, HDiv.hDiv, HAdd.hAdd, HMul.hMul, HSub.hSub, HPow.hPow, Or, Dvd.dvd

    Proof uses: LT.lt, Trans.trans, Eq.symm, pow_one, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.mul_pos, pow_pos, Eq.mp, congrArg, propext, div_eq_div_iff, cast, Not, Eq.trans, Nat.cast_zero and 48 more

    100 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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