[summary: Bézout's theorem states that if $~$a$~$ and $~$b$~$ are integers, and $~$c$~$ is an integer, then the equation $~$ax+by = c$~$ has integer solutions in $~$x$~$ and $~$y$~$ if and only if the Greatest common divisor of $~$a$~$ and $~$b$~$ divides $~$c$~$.]
Bézout's theorem is an important basic theorem of number theory. It states that if $~$a$~$ and $~$b$~$ are integers, and $~$c$~$ is an integer, then the equation $~$ax+by = c$~$ has integer solutions in $~$x$~$ and $~$y$~$ if and only if the Greatest common divisor of $~$a$~$ and $~$b$~$ divides $~$c$~$.
Proof
We have two directions of the equivalence to prove.
If $~$ax+by=c$~$ has solutions
Suppose $~$ax+by=c$~$ has solutions in $~$x$~$ and $~$y$~$. Then the highest common factor of $~$a$~$ and $~$b$~$ divides $~$a$~$ and $~$b$~$, so it divides $~$ax$~$ and $~$by$~$; hence it divides their sum, and hence $~$c$~$.
If the highest common factor divides $~$c$~$
Suppose $~$\mathrm{hcf}(a,b) \mid c$~$; equivalently, there is some $~$d$~$ such that $~$d \times \mathrm{hcf}(a,b) = c$~$.
We have the following fact: that the highest common factor is a linear combination of $~$a, b$~$. ([hcf_is_linear_combination Proof]; this [extended_euclidean_algorithm can also be seen] by working through [euclidean_algorithm Euclid's algorithm].)
Therefore there are $~$x$~$ and $~$y$~$ such that $~$ax + by = \mathrm{hcf}(a,b)$~$.
Finally, $~$a (xd) + b (yd) = d \mathrm{hcf}(a, b) = c$~$, as required.
Actually finding the solutions
Suppose $~$d \times \mathrm{hcf}(a,b) = c$~$, as above.
The [-extended_euclidean_algorithm] can be used (efficiently!) to obtain a linear combination $~$ax+by$~$ of $~$a$~$ and $~$b$~$ which equals $~$\mathrm{hcf}(a,b)$~$. Once we have found such a linear combination, the solutions to the integer equation $~$ax+by=c$~$ follow quickly by just multiplying through by $~$d$~$.
Importance
Bézout's theorem is important as a step towards the proof of Euclid's lemma, which itself is the key behind the Fundamental Theorem of Arithmetic. It also holds in general principal ideal domains.