[proofplan]
The remainders are nonnegative integers and, as long as the algorithm has not stopped, strictly decrease. This proves termination by finiteness. The main invariant is that replacing the pair $(r_{i-1},r_i)$ by $(r_i,r_{i+1})$ preserves the set of common divisors, hence preserves the greatest common divisor. At the final stage the pair is $(r_N,0)$, whose greatest common divisor is $r_N$. When $A/B>0$, the same division identities can be divided by the current denominator to obtain the usual recursive continued fraction identities.
[/proofplan]
[step:Show that the decreasing nonnegative remainders force termination]
For every index $i$ for which the division step is performed, the defining inequalities give
\begin{align*}
0 \leq r_{i+1} < r_i.
\end{align*}
Since $r_0 = B$ and $B > 0$, every positive remainder after $r_0$ is an integer in the finite set
\begin{align*}
\{1,2,\dots,B-1\}.
\end{align*}
Thus the algorithm cannot produce infinitely many positive remainders, because a strictly decreasing sequence of nonnegative integers beginning at $B$ has length at most $B+1$. Therefore there exists an index $N \in \mathbb{N} \cup \{0\}$ such that
\begin{align*}
r_N > 0, \qquad r_{N+1} = 0.
\end{align*}
[/step]
[step:Prove that each division preserves the common divisors]
Fix an index $i$ for which
\begin{align*}
r_{i-1} = a_i r_i + r_{i+1}.
\end{align*}
Let $d \in \mathbb{Z}$. If $d$ divides both $r_{i-1}$ and $r_i$, then $d$ divides
\begin{align*}
r_{i+1} = r_{i-1} - a_i r_i.
\end{align*}
Hence $d$ divides both $r_i$ and $r_{i+1}$. Conversely, if $d$ divides both $r_i$ and $r_{i+1}$, then $d$ divides
\begin{align*}
r_{i-1} = a_i r_i + r_{i+1}.
\end{align*}
Hence $d$ divides both $r_{i-1}$ and $r_i$. Therefore the common divisors of $r_{i-1}$ and $r_i$ are exactly the common divisors of $r_i$ and $r_{i+1}$.
[guided]
Fix an index $i$ at which the algorithm performs the division
\begin{align*}
r_{i-1} = a_i r_i + r_{i+1}.
\end{align*}
We want to prove that the replacement of the pair $(r_{i-1},r_i)$ by the next pair $(r_i,r_{i+1})$ does not change the common divisors. This is the algebraic invariant behind the Euclidean algorithm.
Let $d \in \mathbb{Z}$ be a common divisor of $r_{i-1}$ and $r_i$. By definition, there exist integers $m,n \in \mathbb{Z}$ such that
\begin{align*}
r_{i-1} = dm, \qquad r_i = dn.
\end{align*}
Using the division identity, we compute
\begin{align*}
r_{i+1}
=
r_{i-1} - a_i r_i
=
dm - a_i dn
=
d(m-a_i n).
\end{align*}
Since $m-a_i n \in \mathbb{Z}$, this proves that $d$ divides $r_{i+1}$. Thus every common divisor of $r_{i-1}$ and $r_i$ is a common divisor of $r_i$ and $r_{i+1}$.
Conversely, let $d \in \mathbb{Z}$ be a common divisor of $r_i$ and $r_{i+1}$. Then there exist integers $m,n \in \mathbb{Z}$ such that
\begin{align*}
r_i = dm, \qquad r_{i+1} = dn.
\end{align*}
Substituting into the same division identity gives
\begin{align*}
r_{i-1}
=
a_i r_i + r_{i+1}
=
a_i dm + dn
=
d(a_i m+n).
\end{align*}
Since $a_i m+n \in \mathbb{Z}$, the integer $d$ divides $r_{i-1}$. Thus every common divisor of $r_i$ and $r_{i+1}$ is a common divisor of $r_{i-1}$ and $r_i$.
The two inclusions prove equality of the two sets of common divisors. This is exactly why the Euclidean step is valid: replacing a number by its remainder changes the pair, but not the divisibility information shared by the pair.
[/guided]
[/step]
[step:Iterate the divisor invariant to identify the last nonzero remainder]
By the previous step, for every performed division the pairs $(r_{i-1},r_i)$ and $(r_i,r_{i+1})$ have the same common divisors. Iterating from $i=0$ through $i=N$ shows that $(A,B)=(r_{-1},r_0)$ and $(r_N,r_{N+1})=(r_N,0)$ have the same common divisors.
Since $r_N > 0$, the common divisors of $r_N$ and $0$ are precisely the divisors of $r_N$. The greatest positive common divisor of $r_N$ and $0$ is therefore $r_N$. Because the set of common divisors is unchanged throughout the algorithm, the greatest positive common divisor of $A$ and $B$ is also $r_N$. Hence
\begin{align*}
r_N = \gcd(A,B).
\end{align*}
[/step]
[step:Rewrite the division identities as a finite continued fraction]
Assume now that $A/B > 0$. Since $B>0$, this implies $A>0$. For each $i$ with $0 \leq i \leq N$, define the positive rational number
\begin{align*}
x_i := \frac{r_{i-1}}{r_i}.
\end{align*}
This is well-defined because $r_i>0$ for $0 \leq i \leq N$. Dividing
\begin{align*}
r_{i-1} = a_i r_i + r_{i+1}
\end{align*}
by $r_i$ gives, for $0 \leq i < N$,
\begin{align*}
x_i
=
a_i + \frac{r_{i+1}}{r_i}
=
a_i + \frac{1}{r_i/r_{i+1}}
=
a_i + \frac{1}{x_{i+1}}.
\end{align*}
For the final index $N$, the identity $r_{N-1}=a_N r_N+r_{N+1}$ and $r_{N+1}=0$ give
\begin{align*}
x_N = a_N.
\end{align*}
Substituting the final identity into the previous one, and then proceeding backward from $i=N-1$ to $i=0$, yields
\begin{align*}
\frac{A}{B}
=
x_0
=
a_0 + \cfrac{1}{a_1 + \cfrac{1}{a_2 + \cdots + \cfrac{1}{a_N}}}.
\end{align*}
Thus the Euclidean quotients are exactly the partial quotients in the finite continued fraction expansion of $A/B$.
[/step]
