Bézout's identity: for integers $a, b$ not both zero, $\gcd(a,b)$ is the least positive element of $\{\, ax + by : x, y \in \mathbb{Z} \,\}$; in particular $ax + by = \gcd(a,b)$ has an integer solution

If $0 \le u$ and $0 \le v$ then $0 \le uv$, and if moreover $u \ne 0$ and $v \ne 0$ then $0 < uv$: for $u = 0$ or $v = 0$ the product is $0$, and otherwise $0 < u$ and $0 < v$, so $0 < uv$ because positives are closed under multiplication.

If $0 < u$ and $0 \le v$ then $0 < u + v$: adding $u$ to $0 \le v$ gives $u \le u + v$, so $0 \le u + v$ by transitivity, and $u + v = 0$ would give $u \le 0$ and hence $u = 0$ by antisymmetry, contrary to $0 < u$.

$x \cdot x \ge 0$ for every $x$, with $x \cdot x > 0$ when $x \ne 0$. By totality either $0 \le x$, and step 1.1 applies directly, or $x \le 0$, in which case $0 \le -x$ by compatibility with addition and $x \cdot x = (-x)(-x) \ge 0$ by step 1.1; the strict form follows since $x \ne 0$ gives $-x \ne 0$.

$I$ contains a positive element: $a \cdot a + b \cdot b \in I$, and one of $a, b$ is nonzero, so one of $a \cdot a$, $b \cdot b$ is positive and the other is nonnegative, whence the sum is positive by step 1.2.

Let $P$ be the set of positive elements of $I$ and put $T := \{\, k \in \mathbb{N} : \iota(k) \in P \,\}$. Every $p \in P$ satisfies $p \ge 0$, hence $p = \iota(k)$ for some $k \in \mathbb{N}$ with $k \in T$; so $T$ is nonempty by step 3.1.

By well-ordering let $k_0$ be the least element of $T$ and put $d := \iota(k_0)$, so $d \in P$ and $d > 0$; fix $x_0, y_0 \in \mathbb{Z}$ with $d = a x_0 + b y_0$.

$d$ is the least element of $P$: given $p \in P$, write $p = \iota(k)$ with $k \in T$ as in step 4.1; then $k_0 \le k$, and applying $\iota$, which preserves the order, gives $d = \iota(k_0) \le \iota(k) = p$.

$d \mid a$. By [L5] with divisor $d > 0$ write $a = qd + r$ with $0 \le r < d$. Then $r = a - qd = a - q(a x_0 + b y_0) = a(1 - q x_0) + b(-q y_0)$, so $r \in I$. If $r$ were positive it would lie in $P$, so $d \le r$ by step 6.1, which with $r < d$ contradicts antisymmetry. Hence $r$ is not positive; with $0 \le r$ this forces $r = 0$, so $a = qd$ and $d \mid a$.

$d \mid b$, by the same argument with $b$ in place of $a$: dividing $b$ by $d$ gives $b = q'd + r'$ with $0 \le r' < d$, and $r' = b(1 - q' y_0) + a(-q' x_0) \in I$, so $r' = 0$ as before.

So $d$ is a common divisor of $a$ and $b$. Moreover every common divisor $c$ of $a$ and $b$ divides $a x_0 + b y_0 = d$ by [L7].

Since $d > 0$ we have $d \ne 0$ and $|d| = d$, so every common divisor $c$ satisfies $c \le |d| = d$ by [L8].

Therefore $d$ is the greatest element of $D(a,b)$, and greatest elements are unique, so $d = \gcd(a,b)$ by [L6]; the hypothesis that $a$ and $b$ are not both $0$ is what makes that clause of the definition apply.

Hence $\gcd(a,b) = d$ is the least positive element of $I$ by step 6.1, and $\gcd(a,b) = a x_0 + b y_0$ by step 5.1: the equation $ax + by = \gcd(a,b)$ is solvable.