let m, n, k be Integer; :: thesis: ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )

A1: now

assume A2: m gcd n divides k ; :: thesis: ex x, y being Integer st (m * x) + (n * y) = k

now

consider m1, n1 being Integer such that
A3: m gcd n = (m * m1) + (n * n1) by Th35;
consider l being Integer such that
A4: (m gcd n) * l = k by A2, INT_1:def 9;
k = (m * (m1 * l)) + (n * (n1 * l)) by A4, A3;
hence ex x, y being Integer st (m * x) + (n * y) = k ; :: thesis: verum

end;

hence ex x, y being Integer st (m * x) + (n * y) = k ; :: thesis: verum

end;

now

given x, y being Integer such that A5: (m * x) + (n * y) = k ; :: thesis: m gcd n divides k
( m gcd n divides m & m gcd n divides n ) by INT_2:31;
hence m gcd n divides k by A5, Th10; :: thesis: verum

end;

hence ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k ) by A1; :: thesis: verum