let a1, b1 be Real; :: thesis: for n1, d1 being Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) holds
ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )
let n1, d1 be Integer; :: thesis: ( d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) implies ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) ) )
assume that
A1: d1 > 0 and
A2: |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) ; :: thesis: ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )
set d = ((a1 / b1) + (n1 / d1)) * (d1 |^ 2);
(((a1 / b1) + (n1 / d1)) * (d1 |^ 2)) / (d1 |^ 2) = (a1 / b1) + (n1 / d1) by A1, XCMPLX_1:89;
then A4: (- (a1 / b1)) + ((((a1 / b1) + (n1 / d1)) * (d1 |^ 2)) / (d1 |^ 2)) = n1 / d1 ;
A5: |.(((a1 / b1) + (n1 / d1)) * (d1 |^ 2)).| = |.((a1 / b1) + (n1 / d1)).| * |.(d1 |^ 2).| by COMPLEX1:65
.= |.((a1 / b1) + (n1 / d1)).| * (d1 |^ 2) ;
(1 / ((sqrt 5) * (d1 |^ 2))) * (d1 |^ 2) = ((1 / (sqrt 5)) * (1 / (d1 |^ 2))) * (d1 |^ 2) by XCMPLX_1:102
.= 1 / (sqrt 5) by A1, XCMPLX_1:109 ;
hence ex d being Real st
( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) ) by A4, A1, A2, XREAL_1:68, A5; :: thesis: verum