TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Fermat's little theorem: for prime $p$ , $p\nmid a$ implies $a^{p-1}\equiv1\pmod p$ , and always $a^p\equiv a\pmod p$

Statement

Let $p$ be a prime integer and $a\in\mathbb Z$ . If $p\nmid a$ , then

$a^{p-1}\equiv1\pmod p.$

For every integer $a$ , without the nondivisibility hypothesis,

$a^p\equiv a\pmod p.$

Facts & Assumptions

Given: A prime integer $p$ and an integer $a$ .

[F1]

A prime satisfies $p>1$ , and $p\nmid a$ implies $\gcd(p,a)=1$ , hence $\gcd(a,p)=1$ by symmetry of the gcd (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ , For a prime $p$ and any integer $a$ , $\gcd(p,a)$ is $p$ when $p \mid a$ and $1$ otherwise; so $p \nmid a$ makes $p$ and $a$ coprime, $\gcd$ is symmetric and unchanged by signs: $\gcd(a,b) = \gcd(b,a) = \gcd(|a|,|b|)$ ; moreover $\gcd(a,0) = |a|$ , $\gcd(a,1) = 1$ , $\gcd(a,a) = |a|$ , and $\gcd(a,b) \ge 1$ unless $a = b = 0$ ).

[L1]

Euler's theorem gives $a^{\varphi(p)}\equiv1\pmod p$ when $\gcd(a,p)=1$ , and $\varphi(p)=p-1$ for prime $p$ (Euler's theorem: if $n\ge1$ and $\gcd(a,n)=1$ , then $a^{\varphi(n)}\equiv1\pmod n$ , $\varphi(1)=1$ , and $\varphi(p)=p-1$ for every prime $p$ ).

[F2]

Congruence is preserved by multiplication, and $p\mid x$ is equivalent to $x\equiv0\pmod p$ (Congruent integers may be added, subtracted and multiplied: representative changes preserve both arithmetic operations, Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$ , including the moduli $0$ and $1$ , Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L2]

Integer powers satisfy $a^p=a^{p-1}a$ for the positive exponent $p$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ , Exponent laws in a group: $g^{m+n} = g^{m}g^{n}$ and $(g^{m})^{n} = g^{mn}$ for all $m, n \in \mathbb{Z}$ , and $(gh)^{n} = g^{n}h^{n}$ when $g$ and $h$ commute).

Proof

technique · cases

1.1

Assume first that $p\nmid a$ . Then $\gcd(a,p)=1$ , so [L1] gives $a^{p-1}\equiv1\pmod p$ . Multiplying by $a$ and using [L2] gives $a^p\equiv a\pmod p$ .

assume-case nondivF1L1F2L2

1.2

Assume instead that $p\mid a$ . Then $a\equiv0\pmod p$ , so repeated multiplication gives $a^p\equiv0^p=0\equiv a\pmod p$ .

assume-case divF1F2

2.1

The first assertion is contained in step 1.1, and the two exhaustive cases $p\nmid a$ and $p\mid a$ give the unconditional congruence.

step 1.1step 1.2cases-exhaustive∎

Depends on

Used by

Over Fₚ, xᵖ-x and the zero polynomial induce the same function but are distinct polynomials Counterexample

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 91 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Thomas W. Judson, Abstract Algebra: Theory and Applications, Lagrange's Theorem (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.3: Fermat's and Euler's Theorems (standard reference, not scraped)

Fermat's little theorem: for prime ppp, p∤ap\nmid ap∤a implies ap−1≡1(modp)a^{p-1}\equiv1\pmod pap−1≡1(modp), and always ap≡a(modp)a^p\equiv a\pmod pap≡a(modp)