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

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

end;

now

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

now

consider l being Integer such that
A5: (m gcd n) * l = k by A4, INT_1:def 9;
consider m1, n1 being Integer such that
A6: m gcd n = (m * m1) + (n * n1) by Th35;
k = (m * (m1 * l)) + (n * (n1 * l)) by A5, A6;
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;

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