Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

For every prime pp, the two operations on Z/p\mathbb{Z}/p make it a field

Statement

For every prime pp, the operations of addition and multiplication on Z/p\mathbb Z/p make it a field (Field).

Facts & Assumptions

Given: A prime integer pp.

[L1]

Modular addition makes Z/p\mathbb Z/p an abelian group, modular multiplication makes it a commutative monoid, and both distributive laws hold (For every natural nn, (Z/n,+)(\mathbb{Z}/n,+) is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L3]

For positive modulus pp, [a]p[a]_p is invertible exactly when gcd(a,p)=1\gcd(a,p)=1 (For n1n\ge1, [a]n[a]_n is a unit if and only if gcd(a,n)=1\gcd(a,n)=1).

[L4]

Equality [a]p=[b]p[a]_p=[b]_p is equivalent to ab(modp)a\equiv b\pmod p, which means p(ab)p\mid(a-b) (The congruence class [a]n[a]_n and the quotient set Z/n\mathbb{Z}/n, Congruence modulo an integer: ab(modn)a\equiv b\pmod n when n(ab)n\mid(a-b), including the moduli 00 and 11).

[L5]

A field is a commutative ring with 010\ne1 in which every nonzero element is multiplicatively invertible (Field).

Proof

technique · direct
1.1

By [L1], all additive, multiplicative, identity, inverse, commutativity, associativity and distributive field axioms already hold except possibly [0]p[1]p[0]_p\ne[1]_p and invertibility of nonzero classes.

L1L5
1.2

Since p>1p>1, it does not divide 11, so [L4] gives [0]p[1]p[0]_p\ne[1]_p.

L2L4
1.3

If [a]p[0]p[a]_p\ne[0]_p, then pap\nmid a by [L4]. Hence gcd(a,p)=1\gcd(a,p)=1 by [L2], and [L3] makes [a]p[a]_p invertible.

L2L3L4
2.1

Steps 1.1 through 1.3 verify every clause of [L5], so Z/p\mathbb Z/p is a field.

step 1.1step 1.2step 1.3L5

Depends on

Used by

Dependency tree · next 3 levels

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