let m, n be Nat; :: thesis: ( m,n are_coprime implies ex k being Nat st
( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) ) )
defpred S₁[ Nat] means ex i0, j0 being Integer st
( $1 = (i0 * m) + (j0 * n) & $1 > 0 );
assume A1: m,n are_coprime ; :: thesis: ex k being Nat st
( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) )
( m > 0 or n > 0 )

proof

assume ( not m > 0 & not n > 0 ) ; :: thesis: contradiction
then ( m = 0 & n = 0 ) ;
then m gcd n <> 1 by NAT_D:32;
hence contradiction by A1, INT_2:def 3; :: thesis: verum

end;

then (1 * m) + (1 * n) > 0 ;
then A2: ex k being Nat st S₁[k] ;
consider k being Nat such that
A3: S₁[k] and
A4: for l being Nat st S₁[l] holds
k <= l from NAT_1:sch 5(A2);
take k ; :: thesis: ( ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) & ( for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l ) )
thus ex i0, j0 being Integer st
( k = (i0 * m) + (j0 * n) & k > 0 ) by A3; :: thesis: for l being Nat st ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) holds
k <= l
let l be Nat; :: thesis: ( ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) implies k <= l )
thus ( ex i, j being Integer st
( l = (i * m) + (j * n) & l > 0 ) implies k <= l ) by A4; :: thesis: verum