let m, n be Nat; :: thesis: ( m,n are_relative_prime implies for k being Nat ex i, j being Integer st (i * m) + (j * n) = k )
assume A1: m,n are_relative_prime ; :: thesis: for k being Nat ex i, j being Integer st (i * m) + (j * n) = k
let k be Nat; :: thesis: ex i, j being Integer st (i * m) + (j * n) = k
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 A1, Th10;
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 A7: ex i, j being Integer st
( b = (i * m) + (j * n) & b > 0 ) ; :: thesis: b mod a = 0
assume A8: b mod a <> 0 ; :: thesis: contradiction
consider i, j being Integer such that
A9: ( b = (i * m) + (j * n) & b > 0 ) by A7;
set t1 = i - ((b div a) * i0);
set t2 = j - ((b div a) * j0);
A10: ((b mod a) + (a * (b div a))) - (a * (b div a)) = b - (a * (b div a)) by A5, NAT_D:2;
reconsider c = ((i - ((b div a) * i0)) * m) + ((j - ((b div a) * j0)) * n) as Element of NAT by A4, A9, A10;
c < a by A4, A5, A9, A10, NAT_D:1;
hence contradiction by A3, A4, A8, A9, A10; :: thesis: verum

end;

reconsider 1' = 1, 0' = 0 as Integer ;
A12: 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 (1' * m) + (0' * 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;

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 (0' * m) + (1' * 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;

then a divides m gcd n by A12, NAT_D:def 5;
then a divides 1 by A1, INT_2:def 4;
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