Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Divisibility of 10n−110^n-110n−1 by 777, 131313, 919191 and 819819819

Proved
AlfutovaUstinov.problem_4_108

by evgeth · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

congruenceselementary-number-theorymultiplicative-ordernumber-theory

This is Problem 4.108 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. The problem asks for an exponent nnn such that 10n−110^n-110n−1 is divisible by (a) 777, (b) 131313, (c) 919191, (d) 819819819; the book's answer is n=6n=6n=6.

The formal statement records the complete answer. For every natural number nnn and for each modulus d∈{7, 13, 91, 819}d\in\{7,\,13,\,91,\,819\}d∈{7,13,91,819},

d∣10n−1  ⟺  6∣n.d \mid 10^{n}-1 \iff 6 \mid n .d∣10n−1⟺6∣n.

In particular n=6n=6n=6 is the smallest positive exponent that works in all four cases (note 91=7⋅1391=7\cdot 1391=7⋅13 and 819=9⋅7⋅13819=9\cdot 7\cdot 13819=9⋅7⋅13).

The exercise concerns the multiplicative order of 101010 modulo small primes, which governs the period length of decimal fractions such as 1/71/71/7 and 1/131/131/13.

Formalization Note The four parts are combined into one conjunction of equivalences, quantified over all n∈Nn\in\mathbb Nn∈N (the case n=0n=0n=0 is harmless: 100−1=010^0-1=0100−1=0 is divisible by everything and 6∣06\mid 06∣0). The subtraction 10n−110^n-110n−1 is natural-number subtraction, which is exact because 10n≥110^n\ge 110n≥1.

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

theorem problem_4_108 (n : ℕ) :
    (7 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧ (13 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧
      (91 ∣ 10 ^ n - 1 ↔ 6 ∣ n) ∧ (819 ∣ 10 ^ n - 1 ↔ 6 ∣ n) := by sorry

end AlfutovaUstinov
Source
N. B. Alfutova, A. V. Ustinov, «Алгебра и теория чисел. Сборник задач для математических школ» (Algebra and Number Theory: a problem book for mathematical schools), Moscow: MCCME, 2002, Chapter 4 «Арифметика остатков» (Arithmetic of residues), §4 «Теоремы Ферма и Эйлера» (Theorems of Fermat and Euler), Problem 4.108. Problem text and answer as catalogued on problems.ru, problem 60734: https://problems.ru/view_problem_details_new.php?id=60734

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me