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\mathrm{\ne }0$ and $v\mathrm{\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\mathrm{\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\mathrm{\ne }0$ gives $-x\mathrm{\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^{\mathrm{\prime }}d+r^{\mathrm{\prime }}$ with $0\le r^{\mathrm{\prime }}<d$, and $r^{\mathrm{\prime }}=b(1-q^{\mathrm{\prime }}{y}_0)+a(-q^{\mathrm{\prime }}{x}_0)\in I$, so $r^{\mathrm{\prime }}=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\mathrm{\ne }0$ and $\mathrm{\mid }d\mathrm{\mid }=d$, so every common divisor $c$ satisfies $c\le \mathrm{\mid }d\mathrm{\mid }=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.