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

proof

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;

A10: a divides n

proof

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: a divides n

hence a divides n by NAT_D:6; :: thesis: verum

end;

suppose n > 0 ; :: thesis: a divides n

then (09 * m) + (a9 * n) > 0 ;
then n mod a = 0 by A6;
then n = (a * (n div a)) + 0 by A2, NAT_D:2;
hence a divides n by NAT_D:3; :: thesis: verum

end;

end;

end;

a divides m

proof

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: a divides m

hence a divides m by NAT_D:6; :: thesis: verum

end;

suppose m > 0 ; :: thesis: a divides m

then (a9 * m) + (09 * n) > 0 ;
then m mod a = 0 by A6;
then m = (a * (m div a)) + 0 by A2, NAT_D:2;
hence a divides m by NAT_D:3; :: thesis: verum

end;

end;

end;

then a divides m gcd n by A10, NAT_D:def 5;
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