let k, m, n, m1, n1 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 that
A1: m <> 0 and
A2: n <> 0 and
A3: (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))) )
consider m2, n2 being Integer such that
A4: m = (m gcd n) * m2 and
A5: n = (m gcd n) * n2 and
A6: m2,n2 are_coprime by A1, INT_2:23;
A7: m gcd n <> 0 by A1, INT_2:5;
then A8: m2 = m / (m gcd n) by A4, XCMPLX_1:89;
A9: n2 = n / (m gcd n) by A7, A5, XCMPLX_1:89;
A10: n2 gcd m2 = 1 by A6, INT_2:def 3;
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 (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))) )
then m * (x - m1) = n * (n1 - y) by A3;
then A11: m2 * (x - m1) = (n * (n1 - y)) / (m gcd n) by A8, XCMPLX_1:74
.= n2 * (n1 - y) by A9, XCMPLX_1:74 ;
then n2 divides m2 * (x - m1) ;
then n2 divides x - m1 by A10, Th29;
then consider t being Integer such that
A12: n2 * t = x - m1 ;
A13: n2 <> 0 by A2, A5;
then A14: t = (x - m1) / n2 by A12, XCMPLX_1:89;
A15: m2 <> 0 by A1, A4;
then (x - m1) / n2 = (n1 - y) / m2 by A13, A11, XCMPLX_1:94;
then t * m2 = n1 - y by A15, A14, XCMPLX_1:87;
then A16: y = n1 - (t * m2) ;
x = m1 + (t * n2) by A12;
hence ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) by A8, A9, A16; :: thesis: verum