TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 ∤ a$ implies $a^{p - 1} \equiv 1 (m o d p)$ , and always $a^{p} \equiv a (m o d p)$

Statement

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

$a^{p - 1} \equiv 1 (m o d p) .$

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

$a^{p} \equiv a (m o d p) .$

Facts & Assumptions

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

[F1]

A prime satisfies $p > 1$ , and $p ∤ 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 ∣ a$ and $1$ otherwise; so $p ∤ 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) \geq 1$ unless $a = b = 0$ ).

[L1]

Euler's theorem gives $a^{φ (p)} \equiv 1 (m o d p)$ when $\gcd (a, p) = 1$ , and $φ (p) = p - 1$ for prime $p$ (Euler's theorem: if $n \geq 1$ and $\gcd (a, n) = 1$ , then $a^{φ (n)} \equiv 1 (m o d n)$ , $φ (1) = 1$ , and $φ (p) = p - 1$ for every prime $p$ ).

[F2]

Congruence is preserved by multiplication, and $p ∣ x$ is equivalent to $x \equiv 0 (m o d p)$ (Congruent integers may be added, subtracted and multiplied: representative changes preserve both arithmetic operations, Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ 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^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

Proof

technique · cases

1.1

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

assume-case nondivF1L1F2L2

1.2

Assume instead that $p ∣ a$ . Then $a \equiv 0 (m o d p)$ , so repeated multiplication gives $a^{p} \equiv 0^{p} = 0 \equiv a (m o d p)$ .

assume-case divF1F2

2.1

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

step 1.1step 1.2cases-exhaustive∎

Depends on

Used by

Dependency tree · two levels

46 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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 pp, p∤ap∤a implies ap−1≡1(modp)ap−1≡1(modp), and always ap≡a(modp)ap≡a(modp)