If $17\nmid n$ , then $17$ divides $n^8+1$ or $n^8-1$

Proved

AlfutovaUstinov.problem_4_123

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

congruenceselementary-number-theoryfermat-little-theoremnumber-theory

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

Theorem. Let $n$ be a natural number that is not divisible by $17$ . Then

17 \mid n^{8}+1 \quad\text{or}\quad 17 \mid n^{8}-1 .

This is a direct application of Fermat's little theorem for the prime $17$ , where $17-1=16=2\cdot 8$ .

Formalization Note The number $n$ is a natural number, as in the book. The expression $n^8-1$ uses natural-number subtraction, which is exact here: the hypothesis $17\nmid n$ forces $n\ge1$ , hence $n^8\ge1$ .

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_123 (n : ℕ) (hn : ¬ 17 ∣ n) : 17 ∣ n ^ 8 + 1 ∨ 17 ∣ n ^ 8 - 1 := 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.123. Problem text and answer as catalogued on problems.ru, problem 60749: https://problems.ru/view_problem_details_new.php?id=60749

View graph

If 17∤n17\nmid n17∤n, then 171717 divides n8+1n^8+1n8+1 or n8−1n^8-1n8−1

If $17\nmid n$ , then $17$ divides $n^8+1$ or $n^8-1$