TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-31

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.

Wilson's theorem: for every prime $p$ , $(p - 1)! \equiv - 1 (m o d p)$

Statement

For every prime $p$ ,

$(p - 1)! \equiv - 1 (m o d p) .$

Facts & Assumptions

Given: A prime $p$ .

[L1]

The unit classes modulo $p$ other than $[1]_{p}$ and $[- 1]_{p}$ occur in disjoint inverse pairs, while those displayed classes are the only self-inverse ones; at $p = 2$ they coincide (In $(Z / p)^{\times}$ , inversion pairs every class except $[1]_{p}$ and $[- 1]_{p}$ , which are the only self-inverse classes).

[L2]

The nonzero standard representatives modulo $p$ are $1, \dots, p - 1$ , and their product is $(p - 1)!$ (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L3]

A finite product in a commutative monoid may be regrouped and reordered, and each inverse pair has product $1$ (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either, For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

Equality of residue classes modulo $p$ is equivalent to congruence modulo $p$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ), and congruence means divisibility of the difference (Congruence modulo an integer: $a \equiv b (m o d n)$ when $n ∣ (a - b)$ , including the moduli $0$ and $1$ ).

[L5]

The quotient $Z / p$ is a field, so every nonzero class is a unit (For every prime $p$ , the two operations on $Z / p$ make it a field).

[F1]

Products of residue classes are computed by multiplying representatives: $[a]_{p} [b]_{p} = [a b]_{p}$ (Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ ).

Proof

technique · direct

1.1

By [L5], the nonzero classes are exactly the unit classes. Multiply them all and regroup by [L1]: every two-element inverse pair contributes $[1]_{p}$ . If the two displayed self-inverse classes are distinct, their contribution is $[1]_{p} [- 1]_{p} = [- 1]_{p}$ ; if they coincide, their single common contribution is itself $[- 1]_{p}$ . Thus in every case the product of all nonzero classes is $[- 1]_{p}$ .

L1L3L5

2.1

By [L2] and [F1], that same class product is $[(p - 1)!]_{p}$ . Therefore $[(p - 1)!]_{p} = [- 1]_{p}$ , which is exactly $(p - 1)! \equiv - 1 (m o d p)$ by [L4].

step 1.1L2L4F1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

Mathematics LibreTexts, Wilson's Theorem (standard reference, not scraped)

Wilson's theorem: for every prime pp, (p−1)!≡−1(modp)(p−1)!≡−1(modp)