let k, m, n, m1, n1 be Integer; ( 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
; 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; ( (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
; 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; verum