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

A1: now :: thesis: ( m gcd n divides k implies ex x, y being Integer st (m * x) + (n * y) = k )

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

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

consider m1, n1 being Integer such that
A3: m gcd n = (m * m1) + (n * n1) by Th28;
consider l being Integer such that
A4: (m gcd n) * l = k by A2;
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 :: thesis: ( ex x, y being Integer st (m * x) + (n * y) = k implies m gcd n divides k )

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:21;
hence m gcd n divides k by A5, Th5; :: 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