# Euclidean division algorithm

($1)$2 | $3 ($4) | $5 ($6)

While studying number theory, we will be primarily interested in the properties of the integers and natural numbers. This means that if we want to write something like "", we'll have to be very careful to check that divides . This makes everything very complicated, so instead, we'll avoid dividing natural numbers.

We can, however, do division with remainder. The Euclidean division algorithm is just a fancy way of saying this:

For all and all , there exists numbers and such that

Here and are the quotient and remainder of over :

Definition: Quotient
We say is a quotient of over if for some with . We write (note that quot is a well defined function).
Definition: Remainder
We say is a remainder of over if for some and . We write (note that rem is a well defined function).

Note that all this is a theorem, it is called the "Euclidean division algorithm" because its proof contains an algorithm.

Proof:
We prove this by weak induction on . Let be the statement "for all , there exists satisfying (1) and (2) above." We will show and assuming .

Base case: We want to show P(0). Let . Then and since .

Inductive step: Assume ; we want to show . By , we know that there exists numbers and such that . We want to show that there exists numbers and such that .

Since , we know that either or . In the former case, we can let and . Then (and clearly ).

In the latter case, we can let and . Then . Again it is clear that .

In either case, we have shown that there exist and satisfying (1) and (2), as required.

Note that even though this is a proof, it also contains an algorithm for finding the quotient and remainder. If , follow the instructions in the base case; if , then first find the quotient q' and remainder r' for and , then follow the instructions in the inductive step. Of course, while we are finding and , we may need to also find and of and .

This is a general pattern: most proofs that something exists give you instructions for finding it. In fact, there are whole programming languages where instead of writing a program, you write a proof; after the computer checks your proof, it extracts a program for you (which is guaranteed to be correct!).