Finite integral domain: deciding ℤ/5ℤ and ℤ/6ℤ from complete tables, then deriving invertibility from finiteness

Goal and scope

Using complete multiplication tables, decide that ℤ/5ℤ is a finite integral domain and ℤ/6ℤ is not; then prove, as a theorem that comes after the definition, that every nonzero element of any finite integral domain is invertible, using finiteness; find all inverses in ℤ/5ℤ and explain why 2 has no inverse in ℤ/6ℤ.

Works inside the MKO's scope: the parent structure already is a complete finite commutative unital ring (ℤ/5ℤ and ℤ/6ℤ, with tables given by reduction modulo n, assumption a1), and the no-zero-divisor condition is quantified over every pair of nonzero elements (assumption a2). The invertibility theorem is proved for a general finite integral domain. It does not prove the general criterion that ℤ/nℤ is a domain exactly when n is prime, and does not set up the finite-field node; it does not change the canonical MKO or its English edition.

Givens and symbols

• divides_def
• division_algorithm
• distributive
• finite_counting_basics
• quantifier_negation
• injective_surjective_def
• case_analysis

• G1 — R5=ℤ/5ℤ={0,1,2,3,4}, with addition and multiplication given by the integer operation followed by the remainder on division by 5; this fixes the complete addition and multiplication tables, and R5 already is a finite commutative unital ring (MKO assumption a1).
• G2 — R6=ℤ/6ℤ={0,1,2,3,4,5}, with the same operations taken modulo 6; R6 also is a finite commutative unital ring.
• G3 — Definition D(R): a finite commutative unital ring R is a finite integral domain if 1≠0 and, for all a,b∈R, a≠0 and b≠0 ⇒ ab≠0 (quantified over every pair of nonzero elements, MKO assumption a2). The definition contains no clause about nonzero elements being invertible.

• \mathbb{Z}/n\mathbb{Z} — integers modulo n, elements written 0 to n−1
• D(R) — R is a finite integral domain
• \lambda_a — the multiplication map x↦ax
• a^{-1} — the multiplicative inverse of a
• R\setminus\{0\} — the nonzero elements of R

Rules and sources

• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• mko_fid_def · cited — Using the same complete finite commutative unital-ring tables, require a*b to differ from zero for every pair of nonzero elements. The complete table supports an exhaustive zero-divisor audit. Invertibility of every nonzero element is a subsequent theorem using finiteness, not silently inserted into this definition. · mko-finite-integral-domain
• mod_reduce · prerequisite — In ℤ/nℤ an integer m stands for its remainder r on division by n (0≤r<n); two integers stand for the same element exactly when n divides their difference; the product of two elements is the remainder of the integer product.
• ring_axioms · prerequisite — Commutative unital ring: addition forms a commutative group, multiplication is associative and commutative with identity 1, and distributivity holds; hence a·0=0 and a(x−y)=ax−ay.
• L_lambda_injective · lemma — In an integral domain R, if a≠0 then λ_a(x)=ax is injective: ax=ay ⇒ x=y.
• L_finite_inj_surj · lemma — An injective map f:S→S on a finite set S is surjective.

Main derivation

D(\mathbb{Z}/5\mathbb{Z})

\text{(i) ring (G1)}\ \land\ \text{(ii) }1\neq 0\ \land\ \text{(iii) }\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

1,0\in\mathbb{Z}/5\mathbb{Z}

1\neq 0

\forall (a,b)\in\{1,2,3,4\}^2:\ ab\neq 0

\forall a\le b\ \text{in}\ \{1,2,3,4\}:\ ab\neq 0

ab\ (1\le a\le b\le 4)\ \text{in}\ \mathbb{Z}/5\mathbb{Z}

1\cdot b=b;\ 2\cdot2=4,\ 2\cdot3=1,\ 2\cdot4=3,\ 3\cdot3=4,\ 3\cdot4=2,\ 4\cdot4=1

\text{the 10 products lie in }\{1,2,3,4\}

\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

\text{(i)},\ \text{(ii)},\ \text{(iii) for }R_5

D(\mathbb{Z}/5\mathbb{Z})

2,3\in R_6\setminus\{0\}

2\cdot 3=0\ \text{in}\ \mathbb{Z}/6\mathbb{Z},\ \text{hence}\ \neg D(\mathbb{Z}/6\mathbb{Z})

D(R),\ a\in R\setminus\{0\},\ \lambda_a(x)=ax

\lambda_a:R\to R\ \text{injective}

\lambda_a:R\to R\ \text{injective},\ R\ \text{finite}

\lambda_a(R)=R

1\in R=\lambda_a(R)

\exists b\in R:\ ab=ba=1

\lambda_2\ \text{on}\ \mathbb{Z}/5\mathbb{Z}

(0,1,2,3,4)\mapsto(0,2,4,1,3);\ 2^{-1}=3,\ 3^{-1}=2,\ 4^{-1}=4,\ 1^{-1}=1

\lambda_2\ \text{on}\ \mathbb{Z}/6\mathbb{Z}

(0,1,2,3,4,5)\mapsto(0,2,4,0,2,4);\ 1\notin\lambda_2(R_6)

2b=1,\ b\in\mathbb{Z}

\text{no solution: }2\ \text{is not invertible in}\ \mathbb{Z}

D(\mathbb{Z}/5\mathbb{Z}),\ \neg D(\mathbb{Z}/6\mathbb{Z}),\ \text{S08 to S10}

\mathbb{Z}/5\mathbb{Z}\ \text{finite integral domain};\ \mathbb{Z}/6\mathbb{Z}\ \text{not};\ D(R)\Rightarrow\text{every }a\neq0\ \text{invertible}

Substeps and lemmas

1\cdot b,\ b\in\{1,2,3,4\}

1\cdot b=b\neq 0

2\cdot2,\ 2\cdot3,\ 2\cdot4,\ 3\cdot3,\ 3\cdot4,\ 4\cdot4

4,\ 1,\ 3,\ 4,\ 2,\ 1

ax=ay

a(x-y)=0

a(x-y)=0,\ a\neq 0

x=y

\lambda_a\ \text{injective}

|\lambda_a(R)|=|R|

\lambda_a(R)\subseteq R,\ |\lambda_a(R)|=|R|

\lambda_a(R)=R

Reverse audits

• S14 · sufficient_goal_reduction · S06, S07, S10, S11 — Goal G: decide the two rings and prove the invertibility theorem. Sufficient condition H: S06, S07, S10 and S11; H⇒G by conjunction. H is proved forwards from G1 to G3; G is never used as a premise, and invertibility is never made part of the definition.
• S13 · premise_audit · divides_def, zero_product — ℤ is outside the domain of D (which concerns finite rings); it is used here only as a contrast showing what finiteness does.
• S12 · premise_audit · S07, mod_reduce — The six values can be recomputed one by one; that 1 is not in the image is a complete check over all 6 inputs.
• S11 · premise_audit · S06, S10, S04.2, mod_reduce — Each inverse can be checked by multiplying back; these computations are an instance of S10 in one example and do not replace its general proof.
• S10 · premise_audit · S09, image_preimage_def, ring_axioms — It needs the surjectivity of S09; no converse is claimed, and invertibility is not turned back into a clause of D(R).
• S09.2 · premise_audit · S09.1, finite_counting_basics, contradiction — The count |A∪B|=|A|+|B| gives a contradiction only for finite sets; an infinite set can be as large as a proper subset.
• S09.1 · premise_audit · S08, finite_counting_basics, image_preimage_def — It needs injectivity; a non-injective map (such as λ_2 on ℤ/6ℤ) has a smaller image.
• S09 · premise_audit · S08, L_finite_inj_surj — It needs both injectivity and finiteness; for infinite sets it fails: x↦2x on ℤ is injective but not surjective.
• S08.2 · premise_audit · S08.1, G3, contrapositive — This uses the contrapositive form of (iii); without (iii), 2(3−0)=0 with 3−0≠0 in ℤ/6ℤ is exactly a counterexample.
• S08.1 · inverse_equivalence · distributive, eq_congruence, add_inverse — Adding and subtracting ay undo each other and distributivity is an identity, so the step holds both ways.
• S08 · premise_audit · G3, L_lambda_injective — It needs a≠0 and clause (iii) of the definition; in ℤ/6ℤ with a=2 the conclusion fails (S12).
• S07 · premise_audit · G2, mod_reduce, quantifier_negation — One zero-divisor pair is enough; this step does not claim to list all zero divisors.
• S06 · premise_audit · S01, S02, S05, G1 — All three items are needed; invertibility is not used in this step.
• S05 · premise_audit · S03, S04, case_analysis — It needs the cases to be complete (the reduction of S03 and the full list of S04); checking only some of the products cannot establish the universal statement.
• S04.2 · inverse_equivalence · mod_reduce, division_algorithm — Backward check: 4−4, 6−1, 8−3, 9−4, 12−2, 16−1 are 0, 5, 5, 5, 10, 15, all multiples of 5; the remainder is unique by the division algorithm.
• S04.1 · inverse_equivalence · mul_one — 1·b=b is an identity; reading it right to left is the backward direction.
• S04 · inverse_equivalence · mod_reduce, numeric_evaluation — Each result can be checked backwards: the integer product minus the stated remainder is a multiple of 5, so both sides name the same element.
• S03 · inverse_equivalence · mul_comm, forall_elim — Both directions have reasons: specialization gives ⇒ and commutativity gives ⇐. The reduction lowers the amount of computation, not the set of cases covered.
• S02 · premise_audit · mod_reduce, divides_def — Only 5∤1 is needed. In ℤ/1ℤ, 1−0=1 is a multiple of 1, so 1=0 and condition (ii) would fail.
• S01 · premise_audit · G1, G3, mko_fid_def — This step only unfolds the definition and derives no new fact; if any one of the three fails, D(R5) fails.

Error controls and negative controls

Sampled products are not a certificate

The misconception identified in the MKO: declaring no zero divisors after spot checks. In ℤ/6ℤ, 1·5=5, 5·5=25≡1, 2·2=4, 3·3=9≡3, 4·4=16≡4 and 2·5=10≡4 are all nonzero, yet 2·3≡0 and 3·4≡0. This guide selects exhaustive checking of all nonzero pairs as its certificate (ℤ/6ℤ has 5+C(5,2)=15 unordered pairs, N9), as in S03 to S05 for ℤ/5ℤ. It is not the only possible proof: independently verify an inverse for every nonzero a, then multiply ab=0 by that inverse to get b=0. Those inverse witnesses must be checked independently, not obtained circularly from the later theorem that first assumes an integral domain.

Invertibility is not part of the definition

The second misconception identified in the MKO is to put 'nonzero elements are invertible' straight into the definition. Here it is a theorem in S08 to S10, and the only use of finiteness is S09. ℤ has no zero divisors but 2 is not invertible (S13), so without finiteness the theorem fails.

Compute in ℤ/nℤ, not in ℤ

2·3=6 is nonzero in ℤ, but in ℤ/6ℤ the remainder of 6 is 0. Every product must be reduced modulo n before deciding whether it is 0 (S04.2, S07).

• In ℤ/6ℤ the spot checks 1·5, 5·5, 2·2 and 3·3 are nonzero, so ℤ/6ℤ is an integral domain → reject — 2·3=6≡0 with 2 and 3 nonzero; sampling cannot prove a universal statement.
• By definition, every nonzero element of an integral domain is invertible → reject — The definition only requires no zero divisors; 2 is not invertible in ℤ. Invertibility in a finite integral domain is a theorem proved using finiteness.
• The row of 0 in the multiplication table is all zeros, so every ring has zero divisors → reject — Zero divisors need both factors nonzero; a·0=0 does not count. ℤ/5ℤ has none (S05).
• The zero ring {0} has no pairs of nonzero elements, so it is a finite integral domain → reject — The definition requires 1≠0; in the zero ring 1=0.

Result and limitations

ℤ/5ℤ is a finite integral domain: 1≠0, and exhausting all 16 nonzero ordered pairs (reduced to 10 products) gives no zero product. ℤ/6ℤ is not: 2·3=0. In any finite integral domain multiplication by a nonzero a is injective, finiteness makes it surjective, and so a is invertible; in ℤ/5ℤ, 2^{-1}=3, 3^{-1}=2, 4^{-1}=4 and 1^{-1}=1. Invertibility is a theorem after the definition, and ℤ shows it can fail without finiteness.

• This guide does not prove the general criterion 'ℤ/nℤ is a domain exactly when n is prime'; it decides only n=5 and n=6 from complete tables. The finite-field node (the MKO's next step) is separate; this guide only notes that S10 makes the nonzero elements of ℤ/5ℤ invertible.

Verification and source binding

9 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 6842601da20f360629d3dee64daf3c9fc262cafcaa31e16bfde9af109e74d478
• original source SHA-256: c6d77ede514c66536e880f8031f33ef853dd3bf2f798b17a549fcac1447b8f09
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)