Skip to content
Axiomatic Wiki
Theorem·T25

Bezout's identity

The greatest common divisor of two naturals is an integer combination of them.

For not both , there exist such that with from D057, from D058 and D060, and from D055.
In words
For any two natural numbers a and b, not both zero, there exist integers x and y such that a times x plus b times y equals the greatest common divisor of a and b, computed in the integers.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    By strong induction on : let (Separation). It suffices to show: if every lies in , then .
  2. 2
    Case : then , and by T19. Take , . Using the unity and identity laws of T23 and T22, and zero times anything is zero: so .
  3. 3
    Case : by T10 write with . Since , the pair is not both , so the induction hypothesis (as ) gives with and by the recursive clause of T19 (valid since ).
  4. 4
    Applying to and using the embedding preserves addition and multiplication: Adding to both sides and simplifying with the group laws of T22 (associativity, the inverse and identity laws):
  5. 5
    Substituting into the induction-hypothesis equation and expanding with distributivity and the sign rule for negating a product: Rearranging with the commutativity/associativity of T22 and factoring out of the two terms carrying it, using distributivity and commutativity/associativity of :
  6. 6
    So and satisfy : .
  7. 7
    Both cases give , so T08 yields : Bezout's identity holds for every not both .
∎

Remarks

The extended Euclidean algorithm: running the division steps of T19 forward and undoing them, using the group structure of T22, produces the coefficients . This is exactly the identity flagged as awaiting the integers in the notes of T19. In particular, when ( coprime), this exhibits as an integer combination of and , the key fact behind modular inverses; that development (congruence mod , the quotient ring , and Fermat/Euler via L36) is not carried out yet in this library.
Wikipedia ↗Nat.gcd_eq_gcd_ab ↗
Propose an edit1 published revision