Rings of integers are Dedekind domains

By [F1], $\mathbb{Z}$ is a domain. A fraction $a\mathrm{/}b$ equals $c\mathrm{/}d$ in $\mathrm{Frac}(\mathbb{Z})$ exactly when $u(ad-cb)=0$ for some nonzero $u\in \mathbb{Z}$; the domain property makes this equivalent to $ad=cb$, the relation defining $\mathbb{Q}$. The operations agree under $(a,b)\mapsto j(a)\mathrm{/}j(b)$, so this gives the canonical identification $\mathrm{Frac}(\mathbb{Z})=\mathbb{Q}$.

Let $I$ be an ideal of $\mathbb{Z}$. It is an additive subgroup, so [F2] gives $I=n\mathbb{Z}$ for some $n\in \mathbb{N}$; as a $\mathbb{Z}$-module, $I$ is generated by that one element, including when $n=0$. Every submodule of the left regular module $\mathbb{Z}$ is such an ideal. Therefore this module is Noetherian, and $\mathbb{Z}$ is a Noetherian ring by [F11].

The field $\mathbb{Q}$ has characteristic zero: for every positive integer $m$, $m\cdot 1_{\mathbb{Q}}=j(m)\mathrm{\ne }0$ by the injectivity in [F10]. By [F5], $\mathbb{Q}$ is perfect.

Let $P$ be a nonzero prime ideal of $\mathbb{Z}$. By [F2], $P=p\mathbb{Z}$ for a positive integer $p$; since $P$ is proper, $p\mathrm{\ne }1$, so $p>1$. If $p\mid ab$, then $ab\in P$, and [F13] gives $a\in P$ or $b\in P$, so $p\mid a$ or $p\mid b$. The Euclid-property characterization therefore makes $p$ a prime integer.

If $x\in \mathrm{Frac}(\mathbb{Z})$ is integral over $\mathbb{Z}$, step 1.1 identifies it with a rational number, and [F3] gives $x\in \mathbb{Z}$. Hence $\mathbb{Z}$ is integrally closed by [F12].

Put $n=[K:\mathbb{Q}]$, which is finite and at least $1$ by [F4] and because $K$ is a field extension of $\mathbb{Q}$. For each $\alpha \in K$, the $n+1$ vectors $1,\alpha ,\dots ,{\alpha }^n$ in the $n$-dimensional $\mathbb{Q}$-vector space $K$ are linearly dependent, so a nonzero polynomial over $\mathbb{Q}$ vanishes at $\alpha$. Thus $K\mathrm{/}\mathbb{Q}$ is algebraic; [F6] and step 1.3 make it separable.

For the prime $p$ from step 1.4, [F14] makes $\mathbb{Z}\mathrm{/}p$ a field and identifies it with the quotient ring $\mathbb{Z}\mathrm{/}p\mathbb{Z}=\mathbb{Z}\mathrm{/}P$. The quotient criterion in [F14] then makes every nonzero prime ideal of $\mathbb{Z}$ maximal.

First, [F16] gives $0<1<2$, so $2>1$. If $d$ is any positive divisor of $2$, [F15] gives $1\le d\le \mathrm{\mid }2\mathrm{\mid }=2$. If $d\mathrm{\ne }1$, then $1<d$; translation compatibility of the order gives $0<d-1$, and integer discreteness in [F15] gives $1\le d-1$. Hence $2\le d$, so antisymmetry and $d\le 2$ give $d=2$. Thus the only positive divisors of $2$ are $1$ and $2$, and [F17] proves that $2$ is prime. Now [F14] makes $2\mathbb{Z}$ maximal, and [F18] makes it prime. Since $\mathbb{Z}$ is a domain, $(0)$ is prime; and $2\mathrm{\ne }0$ by [F16], so $(0)⊊2\mathbb{Z}$. Every prime chain with positive length starts at $(0)$ and has length at most $1$, because each nonzero prime is maximal by step 2.3. Thus [F19] gives $\dim \mathbb{Z}=1$.

Steps 1.1, 1.2, 2.1, and 3.1 show that $\mathbb{Z}$ is a Noetherian integrally closed domain of dimension $1$. Hence [F7] makes $\mathbb{Z}$ a Dedekind domain.

By [F9], ${\mathcal{O}}_K$ is the integral closure of $\mathbb{Z}$ in $K$. Apply [F8] with $R=\mathbb{Z}$, fraction field $\mathbb{Q}=\mathrm{Frac}(\mathbb{Z})$ from step 1.1, and finite separable extension $K\mathrm{/}\mathbb{Q}$ from step 2.2. Under the given Axiom of Choice, this proves that ${\mathcal{O}}_K$ is Dedekind.