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