let q be Real; :: thesis: ( q is Integer & q > 0 implies for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0 **] holds
|.([**q,0 **] - r).| > q - 1 )
assume A1: ( q is Integer & q > 0 ) ; :: thesis: for r being Element of F_Complex st |.r.| = 1 & r <> [**1,0 **] holds
|.([**q,0 **] - r).| > q - 1
let r be Element of F_Complex ; :: thesis: ( |.r.| = 1 & r <> [**1,0 **] implies |.([**q,0 **] - r).| > q - 1 )
assume that
A2: |.r.| = 1 and
A3: r <> [**1,0 **] ; :: thesis: |.([**q,0 **] - r).| > q - 1
set a = Re r;
set b = Im r;
A4: ((Re r) ^2 ) + ((Im r) ^2 ) = 1 ^2 by A2, COMPTRIG:7;

now

assume A5: Re r = 1 ; :: thesis: contradiction
then Im r = 0 by A4;
hence contradiction by A3, A5, COMPLEX1:29; :: thesis: verum

end;

then ( Re r <> 1 & Re r <= 1 ) by A2, COMPLEX1:140;
then A6: Re r < 1 by XXREAL_0:1;
A7: ( Re [**(q - (Re r)),(- (Im r))**] = q - (Re r) & Im [**(q - (Re r)),(- (Im r))**] = - (Im r) ) by COMPLEX1:28;
2 * q > (2 * q) * (Re r) by A6, A1, XREAL_1:159;
then - ((2 * q) * (Re r)) > - (2 * q) by XREAL_1:26;
then (- (2 * q)) + (q ^2 ) < (- ((2 * q) * (Re r))) + (q ^2 ) by XREAL_1:10;
then A8: ((q ^2 ) - ((2 * q) * (Re r))) + 1 > ((q ^2 ) - (2 * q)) + 1 by XREAL_1:10;
reconsider qc = [**q,0 **] as Element of F_Complex ;
A9: |.(qc - r).| >= 0 by COMPLEX1:132;
|.(qc - r).| ^2 = |.([**q,0 **] - [**(Re r),(Im r)**]).| ^2 by COMPLEX1:29
.= |.[**(q - (Re r)),(0 - (Im r))**].| ^2 by POLYNOM5:6
.= ((q - (Re r)) ^2 ) + ((Im r) ^2 ) by A7, COMPTRIG:7
.= ((q ^2 ) - ((2 * q) * (Re r))) + 1 by A4 ;
then |.(qc - r).| ^2 > (q - 1) ^2 by A8;
hence |.([**q,0 **] - r).| > q - 1 by A9, SQUARE_1:118; :: thesis: verum