CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

For prime $p$ and $d \geq 1$ , the congruence $x^{d} \equiv 1 (m o d p)$ has $\gcd (d, p - 1)$ nonzero solutions

Statement

Let $p$ be prime and $d \geq 1$ . The congruence $x^{d} \equiv 1 (m o d p)$ has exactly $\gcd (d, p - 1)$ nonzero residue-class solutions. In particular, it has exactly $d$ solutions when $d ∣ (p - 1)$ .

Facts & Assumptions

Given: A prime $p$ and a positive integer $d$ .

[L1]

$(Z / p)^{\times}$ is cyclic of order $p - 1$ (For every prime $p$ , the multiplicative group $(Z / p Z)^{\times}$ is cyclic).

[L2]

If $g$ has order $p - 1$ , then $g^{u} = 1$ exactly when $(p - 1) ∣ u$ , and its powers with exponents modulo $p - 1$ are distinct (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

[L3]

The greatest common divisor $c = \gcd (d, p - 1)$ divides both $d$ and $p - 1$ (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L4]

Dividing two integers by their nonzero greatest common divisor gives coprime quotients (If $d = \gcd (a, b)$ is nonzero then $a / d$ and $b / d$ are coprime).

[L5]

If two integers are coprime and one divides a product containing the other, it divides the remaining factor (If $\gcd (a, b) = 1$ and $a ∣ b c$ then $a ∣ c$ ; and if $a ∣ c$ , $b ∣ c$ and $\gcd (a, b) = 1$ then $a b ∣ c$ ).

Proof

technique · direct

1.1

Choose a generator $g$ from [L1]. Every nonzero class is uniquely $g^{a}$ with $a$ modulo $p - 1$ .

L1L2choose

1.2

Put $c = \gcd (d, p - 1)$ . Since $p - 1 \geq 1$ , $c$ is nonzero; write $d = c d^{'}$ , $p - 1 = c m^{'}$ , and use [L4] to obtain $\gcd (d^{'}, m^{'}) = 1$ .

L3L4algebra

2.1

By [L2], $(g^{a})^{d} = 1$ exactly when $(p - 1) ∣ a d$ , which by step 1.2 and [L5] is equivalent to $m^{'} ∣ a$ .

step 1.1step 1.2L2L5

3.1

Modulo $p - 1 = c m^{'}$ , precisely the $c$ classes $0, m^{'}, \dots, (c - 1) m^{'}$ satisfy step 2.1, proving the count. If $d ∣ (p - 1)$ then $c = d$ .

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 107 results over 23 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

William Stein, Elementary Number Theory, Proposition 2.5.5 (standard reference, not scraped)

For prime pp and d≥1d≥1, the congruence xd≡1(modp)xd≡1(modp) has gcd⁡(d,p−1)gcd(d,p−1) nonzero solutions