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_{1}[ 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 )

then A2: ex k being Nat st S_{1}[k]
;

consider k being Nat such that

A3: S_{1}[k]
and

A4: for l being Nat st S_{1}[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

( 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

( $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

then
(1 * m) + (1 * n) > 0
;
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 ( m = 0 & n = 0 ) ;

then m gcd n <> 1 by NAT_D:32;

hence contradiction by A1, INT_2:def 3; :: thesis: verum

then A2: ex k being Nat st S

consider k being Nat such that

A3: S

A4: for l being Nat st S

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