Existence of the gcd and the Euclidean algorithm

Proof

1. 1
   Uniqueness, so that 'the' gcd is well posed: if and both satisfy the characterisation for , then each is a common divisor and the other absorbs every common divisor, so and . Since are not both , say ; then and each divide the nonzero and so are themselves nonzero (if then gives , D030). Now L19 (vii) gives and , and antisymmetry of the order (L16 rules out both and ) forces . Existence is proved by strong induction on .
2. 2
   Let (Separation). By T08 it suffices to show: if every lies in , then .
3. 3
   Case : then . Put . Then (L19 (i)) and ((iii)), and any common divisor of and has . So meets the characterisation: .
4. 4
   Case : by T10 write with . As we have by the induction hypothesis, and are not both (since ), so exists (D055): , , and every common divisor of and divides .
5. 5
   is the gcd of . Note first that , since (L12) is a multiple of (D030). Now : from and , transitivity L19 (iv) gives , and with , ((v)). So is a common divisor of and . Conversely, any common divisor of and divides : from and , ((iv)); with , this gives ((vi)). Then is a common divisor of and , hence . Thus satisfies the characterisation for , so .
6. 6
   Both cases give , so T08 yields : the gcd exists for every pair not both , and the two displayed equations compute it.

Used by