let m, n be Nat; :: thesis: ( m,n are_coprime implies for k being Nat ex i, j being Integer st (i * m) + (j * n) = k )

reconsider a9 = 1, 09 = 0 as Integer ;

assume A1: m,n are_coprime ; :: thesis: for k being Nat ex i, j being Integer st (i * m) + (j * n) = k

then consider a being Nat such that

A2: ex i0, j0 being Integer st

( a = (i0 * m) + (j0 * n) & a > 0 ) and

A3: for c being Nat st ex i, j being Integer st

( c = (i * m) + (j * n) & c > 0 ) holds

a <= c by Th9;

let k be Nat; :: thesis: ex i, j being Integer st (i * m) + (j * n) = k

consider i0, j0 being Integer such that

A4: a = (i0 * m) + (j0 * n) and

A5: a > 0 by A2;

A6: for c being Nat st ex i, j being Integer st

( c = (i * m) + (j * n) & c > 0 ) holds

c mod a = 0

then a divides 1 by A1, INT_2:def 3;

then ex b being Nat st 1 = a * b by NAT_D:def 3;

then (i0 * m) + (j0 * n) = 1 by A4, NAT_1:15;

then k = k * ((i0 * m) + (j0 * n))

.= ((k * i0) * m) + (k * (j0 * n)) ;

then k = ((k * i0) * m) + ((k * j0) * n) ;

hence ex i, j being Integer st (i * m) + (j * n) = k ; :: thesis: verum

reconsider a9 = 1, 09 = 0 as Integer ;

assume A1: m,n are_coprime ; :: thesis: for k being Nat ex i, j being Integer st (i * m) + (j * n) = k

then consider a being Nat such that

A2: ex i0, j0 being Integer st

( a = (i0 * m) + (j0 * n) & a > 0 ) and

A3: for c being Nat st ex i, j being Integer st

( c = (i * m) + (j * n) & c > 0 ) holds

a <= c by Th9;

let k be Nat; :: thesis: ex i, j being Integer st (i * m) + (j * n) = k

consider i0, j0 being Integer such that

A4: a = (i0 * m) + (j0 * n) and

A5: a > 0 by A2;

A6: for c being Nat st ex i, j being Integer st

( c = (i * m) + (j * n) & c > 0 ) holds

c mod a = 0

proof

A10:
a divides n
a divides m
then
a divides m gcd n
by A10, NAT_D:def 5;
let b be Nat; :: thesis: ( ex i, j being Integer st

( b = (i * m) + (j * n) & b > 0 ) implies b mod a = 0 )

assume ex i, j being Integer st

( b = (i * m) + (j * n) & b > 0 ) ; :: thesis: b mod a = 0

then consider i, j being Integer such that

A7: b = (i * m) + (j * n) and

b > 0 ;

set t2 = j - ((b div a) * j0);

set t1 = i - ((b div a) * i0);

A8: ((b mod a) + (a * (b div a))) - (a * (b div a)) = b - (a * (b div a)) by A5, NAT_D:2;

then reconsider c = ((i - ((b div a) * i0)) * m) + ((j - ((b div a) * j0)) * n) as Element of NAT by A4, A7;

assume A9: b mod a <> 0 ; :: thesis: contradiction

c < a by A4, A5, A7, A8, NAT_D:1;

hence contradiction by A3, A4, A9, A7, A8; :: thesis: verum

end;( b = (i * m) + (j * n) & b > 0 ) implies b mod a = 0 )

assume ex i, j being Integer st

( b = (i * m) + (j * n) & b > 0 ) ; :: thesis: b mod a = 0

then consider i, j being Integer such that

A7: b = (i * m) + (j * n) and

b > 0 ;

set t2 = j - ((b div a) * j0);

set t1 = i - ((b div a) * i0);

A8: ((b mod a) + (a * (b div a))) - (a * (b div a)) = b - (a * (b div a)) by A5, NAT_D:2;

then reconsider c = ((i - ((b div a) * i0)) * m) + ((j - ((b div a) * j0)) * n) as Element of NAT by A4, A7;

assume A9: b mod a <> 0 ; :: thesis: contradiction

c < a by A4, A5, A7, A8, NAT_D:1;

hence contradiction by A3, A4, A9, A7, A8; :: thesis: verum

then a divides 1 by A1, INT_2:def 3;

then ex b being Nat st 1 = a * b by NAT_D:def 3;

then (i0 * m) + (j0 * n) = 1 by A4, NAT_1:15;

then k = k * ((i0 * m) + (j0 * n))

.= ((k * i0) * m) + (k * (j0 * n)) ;

then k = ((k * i0) * m) + ((k * j0) * n) ;

hence ex i, j being Integer st (i * m) + (j * n) = k ; :: thesis: verum