let rh0 be Element of REAL ; :: thesis: for p, q being Integer st p,q are_coprime holds

ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

let p, q be Integer; :: thesis: ( p,q are_coprime implies ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2 )

assume A1: p,q are_coprime ; :: thesis: ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

consider b being Element of INT such that

A2: |.(rh0 - b).| <= 1 / 2 by GAUSSINT:48;

consider s, t being Integer such that

A3: (s * p) + (t * q) = 1 by A1, Th15;

A4: b * ((s * p) + (t * q)) = b by A3;

set x = - (b * s);

set y = b * t;

X: ( - (b * s) in INT & b * t in INT ) by INT_1:def 2;

((p * (- (b * s))) - (q * (b * t))) + rh0 = rh0 - b by A4;

hence ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2 by A2, X; :: thesis: verum

ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

let p, q be Integer; :: thesis: ( p,q are_coprime implies ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2 )

assume A1: p,q are_coprime ; :: thesis: ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

consider b being Element of INT such that

A2: |.(rh0 - b).| <= 1 / 2 by GAUSSINT:48;

consider s, t being Integer such that

A3: (s * p) + (t * q) = 1 by A1, Th15;

A4: b * ((s * p) + (t * q)) = b by A3;

set x = - (b * s);

set y = b * t;

X: ( - (b * s) in INT & b * t in INT ) by INT_1:def 2;

((p * (- (b * s))) - (q * (b * t))) + rh0 = rh0 - b by A4;

hence ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2 by A2, X; :: thesis: verum