1 Preliminaries

This chapter provides the necessary prerequisites used throughout this project. We begin by introducing the notation that will be employed, followed by essential definitions and preliminary results required for formalising our arguments.

1.1 Notation

In this section, we define the notation and symbols that will be consistently used in this work.

Symbol	Description
$:=$	Definition
$\forall$	Universal quantification
$\exists$	Existential quantification
$\exists!$	Unique existential quantification
$N$	Set of natural numbers
$Z$	Set of integer numbers
$Z_{n}$	Set of integers modulo $n$
$Q$	Set of rational numbers
$X / Y$	Field extension
$[Y : X]$	Degree of field extension
$\times$	Cartesian product
$[n]$	Equivalence class of $n$
$∣$	Divisibility relation
$∤$	Negation of divisibility relation
$gcd$	Greatest common divisor
$ζ_{n}$	Primitive $n$ -th root of unity

1.2 Definitions

In this section, each definition is articulated as clearly as possible to maximise clarity and precision.

Definition 1.1 Monoid

Let $X$ be a non-empty set.
Let $\circ : X \times X \to X$ be an internal composition law on $X$ .

A monoid is a pair $M := (X, \circ)$ satisfying:

$\forall x, y, z \in X, (x \circ y) \circ z = x \circ (y \circ z) = x \circ y \circ z$
$\exists e \in X : \forall x \in X, x \circ e = e \circ x = x$

Definition 1.2 Commutative Monoid

Let $X$ be a non-empty set.
Let $\circ : X \times X \to X$ be an internal composition law on $X$ .

A commutative monoid is a pair $M_{c} := (X, \circ)$ satisfying:

$\forall x, y, z \in X, (x \circ y) \circ z = x \circ (y \circ z) = x \circ y \circ z$
$\exists e \in X : \forall x \in X, x \circ e = e \circ x = x$
$\forall x, y \in X, x \circ y = y \circ x$

Definition 1.3 GCD Monoid

Let $X$ be a non-empty set.
Let $\circ : X \times X \to X$ be an internal composition law on $X$ .

A gcd monoid is a pair $M_{gcd} := (X, \circ)$ satisfying:

$\forall x, y, z \in X, (x \circ y) \circ z = x \circ (y \circ z) = x \circ y \circ z$
$\exists e \in X : \forall x \in X, x \circ e = e \circ x = x$
$\forall x, y \in X, x \circ y = y \circ x$
$\forall x, y \in X, \exists d \in X : (d ∣ x) \land (d ∣ y) \land (\forall c \in X, c ∣ x \land c ∣ y \Rightarrow c ∣ d)$

Definition 1.4 Group

Let $X$ be a non-empty set.
Let $\circ : X \times X \to X$ be an internal composition law on $X$ .

A group is a pair $G := (X, \circ)$ satisfying:

$\forall x, y, z \in X, (x \circ y) \circ z = x \circ (y \circ z) = x \circ y \circ z$
$\exists e \in X : \forall x \in X, x \circ e = e \circ x = x$
$\forall x \in X, \exists x^{'} \in X : x \circ x^{'} = x^{'} \circ x = e$

Definition 1.5 Commutative Group

Let $X$ be a non-empty set.
Let $\circ : X \times X \to X$ be an internal composition law on $X$ .

A commutative group is a pair $G_{c} := (X, \circ)$ satisfying:

$\forall x, y, z \in X, (x \circ y) \circ z = x \circ (y \circ z) = x \circ y \circ z$
$\exists e \in X : \forall x \in X, x \circ e = e \circ x = x$
$\forall x \in X, \exists x^{'} \in X : x \circ x^{'} = x^{'} \circ x = e$
$\forall x, y \in X, x \circ y = y \circ x$

Definition 1.6 Semiring

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A semiring is a triple $S := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.7 Commutative Semiring

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A commutative semiring is a triple $S_{c} := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\forall x, y \in X, x \cdot y = y \cdot x$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.8 Ring

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.9 Commutative Ring

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A commutative ring is a triple $R_{c} := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\forall x, y \in X, x \cdot y = y \cdot x$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.10 Left Ideal

Let $(X, +, \cdot)$ be a ring.

A left ideal is a subset $I \subseteq X$ satisfying:

$(I, +)$ is a subgroup of $(X, +)$
$\forall i \in I, \forall x \in X, x \cdot i \in I$

Definition 1.11 Right Ideal

Let $(X, +, \cdot)$ be a ring.

A right ideal is a subset $I \subseteq X$ satisfying:

$(I, +)$ is a subgroup of $(X, +)$
$\forall i \in I, \forall x \in X, i \cdot x \in I$

Definition 1.12 Ideal

Let $(X, +, \cdot)$ be a ring.

An ideal or two-sided ideal is a subset $I \subseteq X$ satisfying:

$(I, +)$ is a subgroup of $(X, +)$
$\forall i \in I, \forall x \in X, x \cdot i \in I$
$\forall i \in I, \forall x \in X, i \cdot x \in I$

Definition 1.13 Domain

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A domain is a triple $D := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$
$\forall x, y \in X, x \cdot y = 0 \Rightarrow x = 0 \lor y = 0$

Definition 1.14 Commutative Domain

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A commutative or integral domain is a triple $D_{c} := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\forall x, y \in X, x \cdot y = y \cdot x$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$
$\forall x, y \in X, x \cdot y = 0 \Rightarrow x = 0 \lor y = 0$

Definition 1.15 Field

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A field is a triple $F := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x \in X, \exists x^{- 1} \in X : x \cdot x^{- 1} = x^{- 1} \cdot x = 1$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.16 Commutative Field

Let $X$ be a non-empty set.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : X \times X \to X$ be a multiplicative internal composition law on $X$ .

A commutative field is a triple $F_{c} := (X, +, \cdot)$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x, y, z \in X, (x \cdot y) \cdot z = x \cdot (y \cdot z) = x \cdot y \cdot z$
$\forall x, y \in X, x \cdot y = y \cdot x$
$\exists 1 \in X : \forall x \in X, x \cdot 1 = 1 \cdot x = x$
$\forall x \in X, \exists x^{- 1} \in X : x \cdot x^{- 1} = x^{- 1} \cdot x = 1$
$\forall x, y, z \in X, x \cdot (y + z) = x \cdot y + x \cdot z$
$\forall x, y, z \in X, (x + y) \cdot z = x \cdot z + y \cdot z$

Definition 1.17 Fundamental System of Field

Let $(X, +, \cdot)$ be a field endowed with a topology $T$ .
Let $I \subseteq N$ be an index set.

A fundamental system of $X$ is a collection $U = {U_{i}}_{i \in I}$ of open sets in $X$ such that:

$\forall i \in I, 0 \in U_{i}$ .
$\forall V ∋ 0, \exists i \in I : U_{i} \subseteq V$ .

Definition 1.18 Vector Space

Let $X$ be a non-empty set.
Let $(K, +, \cdot)$ be a field.
Let $+ : X \times X \to X$ be an additive internal composition law on $X$ .
Let $\cdot : K \times X \to X$ be a multiplicative external composition law on $X$ .

A $K$ -vector space or $K$ -linear space is a triple $V := (X, +, \cdot)_{K}$ satisfying:

$\forall x, y, z \in X, (x + y) + z = x + (y + z) = x + y + z$
$\forall x, y \in X, x + y = y + x$
$\exists 0 \in X : \forall x \in X, x + 0 = 0 + x = x$
$\forall x \in X, \exists (- x) \in X : x + (- x) = (- x) + x = 0$
$\forall x \in X, \forall k, ℓ \in K, k \cdot_{X} (ℓ \cdot_{X} x) = (k \cdot_{K} ℓ) \cdot_{X} x$
$\exists 1 \in K : \forall x \in X, 1 \cdot x = x$
$\forall x, y \in X, \forall k \in K, k \cdot (x +_{X} y) = k \cdot x +_{X} k \cdot y$
$\forall k, ℓ \in K, \forall x \in X, (k +_{K} ℓ) \cdot x = k \cdot x +_{X} ℓ \cdot x$

From now on, we shall employ the notation $X$ in place of the more explicit $(X, +, \cdot)$ to denote a field, commutative ring, domain, or similar algebraic structures when the context unambiguously implies the operations involved.

Definition 1.19 Field Extension

Let $(X, +, \cdot)$ be a field.
Let $(Y, +, \cdot)$ be a field such that $Y \subseteq X$ .

A field extension is the pair $X / Y$ such that the operations of $Y$ are those of $X$ restricted to $Y$ .

Definition 1.20 Degree of Field Extension

Let $(X, +, \cdot)$ be a field.
Let $(Y, +, \cdot)$ be a field such that $Y \subseteq X$ .
Let $X / Y$ be a field extension.

The degree of $X / Y$ , denoted as $[Y : X]$ , is the dimension of $X$ as a vector space over $Y$ .

Definition 1.21 Algebraic Field Extension

Let $(X, +, \cdot)$ be a field.
Let $(Y, +, \cdot)$ be a field such that $Y \subseteq X$ .

An algebraic field extension is the field extension $X / Y$ such that its degree $[Y : X]$ is finite.

Definition 1.22 Extension Field

Let $(X, +, \cdot)$ be a field.
Let $(Y, +, \cdot)$ be a field such that $Y \subseteq X$ .
Let $X / Y$ be a field extension.

The field $X$ is said to be an extension field of $Y$ .

Definition 1.23 Subfield

Let $(X, +, \cdot)$ be a field.
Let $(Y, +, \cdot)$ be a field such that $Y \subseteq X$ .
Let $X / Y$ be a field extension.

The field $Y$ is said to be a subfield of $X$ .

Definition 1.24 Number Field

Let $(X, +, \cdot)$ be a field.
Let $(Q, +, \cdot)$ be the field of rational numbers such that $Q \subseteq X$ .
Let $X / Q$ be an algebraic field extension.

The extension field $X$ is said to be a number field or an algebraic number field.

Definition 1.25 Root of Unity

Let $n \in N_{+}$ .

A $n$ -th root of unity is an element $ζ \in C$ such that $ζ^{n} = 1$ .

Definition 1.26 Primitive Root of Unity

Let $n \in N_{+}$ .

A primitive $n$ -th root of unity is an element $ζ \in C$ satisfying:

$ζ^{n} = 1$ .
$\forall k \in N_{+}, k < n ⟹ ζ^{k} \neq 1$ .

Definition 1.27 Cyclotomic Polynomial

Let $n \in N_{+}$ .
Let $ζ \in C$ be a primitive $n$ -th root of unity.

The $n$ -th cyclotomic polynomial is the unique monic polynomial with integer coefficients whose roots are the primitive $n$ -th roots of unity:

Φ_{n} (x) = \prod_{\begin{matrix} 1 \leq k \leq n \\ gcd (k, n) = 1 \end{matrix}} (x - ζ^{k})

Definition 1.28 Cyclotomic Extension Field

Let $n \in N_{+}$ .
Let $ζ_{n} \in C$ be a primitive $n$ -th root of unity.
Let $X$ be a field.

The $n$ -th cyclotomic extension field or $n$ -th cyclotomic field is a field $X (ζ_{n})$ obtained by adjoining $ζ_{n}$ to $X$ .

1.3 Results

In this section, we state some preliminary results that are crucial for the development of our formal proofs.

Theorem 1.29

✓

Let $p \in N$ be prime.

If $ζ_{p}$ is a primitive $p$ -th root of unity, then $ζ_{p} - 1$ is prime.

Proof ▶

Lemma 1.30

✓

Let $R$ be a commutative semiring, domain and normalised $gcd$ monoid.
Let $a, b, c \in R$ .
Let $n \in N$ .

Then, to prove Fermat’s Last Theorem for exponent $n$ in $R$ , one can assume, without loss of generality, that $gcd (a, b, c) = 1$ .

Proof ▶

Lemma 1.31

✓

Let $Z_{9}$ be the ring of integers modulo $9$ .
Let $Z_{3}$ be the ring of integers modulo $3$ .
Let $n \in Z_{9}$ .
Let $ϕ : Z_{9} \to Z_{3}$ be the canonical ring homomorphism.
Let $ϕ (n) \neq 0$ .

Then $n^{3} = 1 \lor n^{3} = 8$ .

Proof ▶