Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1988P1

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Nat.ModEq
public import Mathlib.Data.Nat.Prime.Defs
public import Mathlib.Tactic.NormNum.GCD
public import Mathlib.Tactic.Ring

public section


/-!
# 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.]
-/

namespace Usa1988P1

/-!
We model the repeating decimal `0.ab…k⟨pq…u⟩` as follows: `r ≥ 1` is the
number of digits before the repeating part, `s ≥ 1` is the length of the
repeating part, `a` is the integer formed by the digits `ab…k` and `b` is
the integer formed by the digits `pq…u`. The value of the decimal is then

  a / 10^r + b / (10^r * (10^s - 1)) = (a * (10^s - 1) + b) / (10^r * (10^s - 1)).

The last digits of `a` and `b` differ (`k ≠ u`), for otherwise the
repeating part could have been started one digit earlier.
-/

theorem usa1988_p1 {r s : ℕ} (hr : 1 ≤ r) (hs : 1 ≤ s) {a b : ℕ}
    (hab : a % 10 ≠ b % 10) {m n : ℕ} (hn : n ≠ 0) (hmn : m.Coprime n)
    (h : (m : ℚ) / (n : ℚ) = ((a * (10 ^ s - 1) + b : ℕ) : ℚ) /
        ((10 ^ r * (10 ^ s - 1) : ℕ) : ℚ)) :
    2 ∣ n ∨ 5 ∣ n := sorry

end Usa1988P1

File author(s): Kimi K3

This problem has a complete formalized solution.