If $13\mid a^{12}+b^{12}+c^{12}+d^{12}+e^{12}+f^{12}$ , then $13^6\mid abcdef$

Proved

AlfutovaUstinov.problem_4_116

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

elementary-number-theoryfermat-little-theoremnumber-theoryolympiad

This is Problem 4.116 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”.

Theorem. Let $a,b,c,d,e,f$ be integers such that

13 \mid a^{12}+b^{12}+c^{12}+d^{12}+e^{12}+f^{12}.

Then

13^{6} \mid abcdef .

The statement is an olympiad-style consequence of Fermat's little theorem for the prime $13$ : twelfth powers take very few values modulo $13$ .

Formalization Note All six variables are integers ( $\mathbb Z$ ), as in the book, and divisibility is the usual divisibility relation on $\mathbb Z$ .

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_116 (a b c d e f : ℤ)
    (h : 13 ∣ a ^ 12 + b ^ 12 + c ^ 12 + d ^ 12 + e ^ 12 + f ^ 12) :
    13 ^ 6 ∣ a * b * c * d * e * f := 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.116. Problem text and answer as catalogued on problems.ru, problem 60742: https://problems.ru/view_problem_details_new.php?id=60742

View graph

If 13∣a12+b12+c12+d12+e12+f1213\mid a^{12}+b^{12}+c^{12}+d^{12}+e^{12}+f^{12}13∣a12+b12+c12+d12+e12+f12, then 136∣abcdef13^6\mid abcdef136∣abcdef

If $13\mid a^{12}+b^{12}+c^{12}+d^{12}+e^{12}+f^{12}$ , then $13^6\mid abcdef$