let m, n, m1, n1, k be Integer; :: thesis: ( m <> 0 & n <> 0 & (m * m1) + (n * n1) = k implies for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) )
assume A1: ( m <> 0 & n <> 0 & (m * m1) + (n * n1) = k ) ; :: thesis: for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )
let x, y be Integer; :: thesis: ( (m * x) + (n * y) = k implies ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) )
assume A2: (m * x) + (n * y) = k ; :: thesis: ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )
A3: m gcd n <> 0 by A1, INT_2:35;
consider m2, n2 being Integer such that
A4: ( m = (m gcd n) * m2 & n = (m gcd n) * n2 & m2,n2 are_relative_prime ) by A1, INT_2:38;
A5: ( m2 = m / (m gcd n) & n2 = n / (m gcd n) ) by A3, A4, XCMPLX_1:90;
A6: n2 gcd m2 = 1 by A4, INT_2:def 4;
A7: ( m2 <> 0 & n2 <> 0 ) by A1, A4;
m * (x - m1) = n * (n1 - y) by A1, A2;
then A8: m2 * (x - m1) = (n * (n1 - y)) / (m gcd n) by A5, XCMPLX_1:75
.= n2 * (n1 - y) by A5, XCMPLX_1:75 ;
then A9: (x - m1) / n2 = (n1 - y) / m2 by A7, XCMPLX_1:95;
n2 divides m2 * (x - m1) by A8, INT_1:def 9;
then n2 divides x - m1 by A6, Th36;
then consider t being Integer such that
A10: n2 * t = x - m1 by INT_1:def 9;
t = (x - m1) / n2 by A7, A10, XCMPLX_1:90;
then t * m2 = n1 - y by A7, A9, XCMPLX_1:88;
then A11: y = n1 - (t * m2) ;
x = m1 + (t * n2) by A10;
hence ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) by A5, A11; :: thesis: verum