Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

Congruence modulo every integer is an equivalence relation on Z

Statement

For every integer n, the relation a≡b(modn) on Z (Congruence modulo an integer: a≡b(modn) when n∣(a−b), including the moduli 0 and 1) is an equivalence relation (Equivalence relation, equivalence class, and the quotient set A/∼). For n=0 it is equality, and for n=1 it is the universal relation.

Facts & Assumptions

Given: An integer n and integers a,b,c.

[L1]

Divisibility is reflexive and linear: d∣u and d∣v imply d∣ux+vy for all integers x,y; also d∣u implies d∣−u (Divisibility is reflexive and transitive on Z, and is linear: if d∣a and d∣b then d∣ax+by for all integers x,y; also d∣a implies d∣ac, −d∣a and d∣−a).

[F2]

An equivalence relation is reflexive, symmetric and transitive (Equivalence relation, equivalence class, and the quotient set A/∼).

Proof

technique · direct
1.1

Reflexivity: a−a=0=n⋅0, so n∣(a−a) and a≡a(modn).

F1algebra
1.2

Symmetry: if a≡b(modn), then n∣(a−b), hence n∣−(a−b)=b−a, so b≡a(modn).

F1L1
1.3

Transitivity: if a≡b(modn) and b≡c(modn), then n∣(a−b) and n∣(b−c), hence n∣(a−b)+(b−c)=a−c, so a≡c(modn).

F1L1algebra
2.1

Steps 1.1, 1.2 and 1.3 establish the three clauses in [F2], so congruence modulo n is an equivalence relation.

step 1.1step 1.2step 1.3F2
3.1

When n=0, [F1] reads 0∣(a−b), which is equivalent to a=b; when n=1, it always holds because a−b=1⋅(a−b).

F1algebra∎

Depends on

Used by

Dependency tree · two levels

14 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