euclidean algorithm
Let \( m , n \in \mathbb{N}_{1} \) such that \( m > n \), if \( m ~\%~ n > 0 \), then \( \gcd{\left ( m , n \right )} = \gcd{\left ( n , m ~\%~ n \right )} \). Otherwise if \( m ~\%~ n = 0 \), then \( n | m \) and \( \gcd{\left ( m , n \right )} = n \)

If \( m ~\%~ n = 0 \), then \( m = \left ( m / / n \right ) \cdot n \), therefore \( \gcd{\left ( m , n \right )} = \gcd{\left ( \left ( m / / n \right ) \cdot n , n \right )} = n \), so now assume that \( m ~\%~ n > 0 \)

Recall that \( m = \left ( m / / n \right ) \cdot n + m ~\%~ n \), therefore \( m - \left ( m / / n \right ) \cdot n = m ~\%~ n \), so that if \( d \) divides both \( m , n \), then it must divide \( m ~\%~ n \) (and clearly \( n \)), and by the original equation if \( d \) is a divisor of both \( n , m ~\%~ n \) then \( d \) divides \( m \) (and clearly \( n \)).

The above paragraph shows that a number is a divisor of \( m , n \) if and only if it is a divisor of \( n , m ~\%~ n \), which shows that their set of divisors are equal and thus \( \gcd{\left ( m , n \right )} = \gcd{\left ( n , m ~\%~ n \right )} \)

bounded sum implies one less then half
Suppose that \( x , y , b \in \mathbb{N}_{1} \) and \( x < y \) with \( x + y \le b \), then \( x < \frac{b}{2} \)
Suppose for the sake of contradiction that \( x \ge \frac{b}{2} \), then we know that \( y > x \ge \frac{b}{2} \) so therefore \( x + y \gt \frac{b}{2} + \frac{b}{2} = b \), so we have \( x + y > b \) which is a contradiction so that \( x < \frac{b}{2} \).
euclidean algorithm has exponentially decreasing remainders
Let \( a , b \in \mathbb{N}_{1} \) with \( a \ge b \) be two integers, and suppose we will preform the euclidean algorithm on them to compute \( \gcd{\left ( m , n \right )} \), supposing that \( r_{k} \) represents the remainder after \( k \) (where \( k \in \mathbb{N}_{1} \)) steps into the euclidean algorithm, then \( r_{2 n} \lt \frac{b}{2^{n}} \)

For the base case, suppose that \( n = 1 \), so we'd like to prove that \( r_{2} \lt \frac{b}{2} \). Firstly we know that \( a = b q_{0} + r_{0} \) with \( 0 \le r_{0} \lt b \), then applying the next iteration we have \( b = r_{0} q_{1} + r_{1} \) with \( 0 \le r_{1} \lt r_{0} \) and one more time, we get \( r_{0} = r_{1} q_{2} + r_{2} \) with \( 0 \le r_{2} \lt r_{1} \), this shows us that \( b = \left ( r_{1} q_{2} + r_{2} \right ) q_{1} + r_{1} \).

Since \( a \ge b \), \( b \gt r_{0} \) and \( r_{0} \gt r_{1} \), then \( q_{0} \ge 1 \), \( q_{1} \ge 1 \) and \( q_{2} \ge 1 \), therefore \( b = \left ( r_{1} q_{2} + r_{2} \right ) q_{1} + r_{1} \ge \left ( r_{1} \cdot 1 + r_{2} \right ) \cdot 1 + r_{1} \ge r 1 + r 2 \) therefore \( r_{2} < \frac{b}{2} \) which concludes the base case

Now let \( k \in \mathbb{N}_{1} \) assuming that \( r_{2 k} \le \frac{b}{2^{k}} \), we want to prove that \( r_{2 \left ( k + 1 \right )} = \frac{b}{2^{k + 1}} \), noting that \( 2 \left ( k + 1 \right ) = 2 k + 2 \).

To start let's say we have an intance of the euclidean algorithm that lasts for at least \( 2 k + 2 \) iterations, therefore we know that \( r_{2 k} \le \frac{b}{2^{k}} \) by our induction hypothesis, additionally at the \( 2 k \)-th iteration we would have an equation of the form \( r_{2 k} = r_{2 k + 1} \left ( q_{2 k + 2} \right ) + r_{2 k + 2} \), since we know that \( r_{2 k + 1} > r_{2 k + 2} \), then \( q_{2 k + 2} \ge 1 \), which then shows that \( r_{2 k} = r_{2 k + 1} \left ( q_{2 k + 2} \right ) + r_{2 k + 2} \ge r_{2 k + 1} + r_{2 k + 1} \), and since \( \frac{b}{2^{k}} \gt r_{2 k} \) , then we know that \( r_{2 k + 2} \lt \frac{1}{2} \cdot \frac{b}{2^{k}} = \frac{b}{2^{k + 1}} \) which is what we needed to show

upper bound on euclidean algorithm iterations
The euclidean algorithm terminates in at most \( 2 \log_{2}{\left ( b \right )} \) iterations
The euclidean algorithm terminates in \( k \) iterations if and only if \( r_{k} = 0 \), we know that for all \( n \in \mathbb{N}_{1} \) that \( r_{2 n} \lt \frac{b}{2^{n}} \), therefore when \( n = \log_{2}{\left ( b \right )} \), then we have \( r_{2 \log_{2}{\left ( b \right )}} \lt \frac{b}{2^{\log_{2}{\left ( b \right )}}} = \frac{b}{b} = 1 \), but if \( r_{2 \log_{2}{\left ( b \right )}} \lt 1 \), then since the remainders are always elements of \( \mathbb{N}_{0} \), then we know that \( r_{2 \log_{2}{\left ( b \right )}} = 0 \), thus we've shown after \( 2 \log_{2}{\left ( b \right )} \) iterations the algorithm must terminate