let q be Real; :: thesis: ( 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 > 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 b = Im r;
set a = Re r;
A4: ((Re r) ^2) + ((Im r) ^2) = 1 ^2 by A2, COMPTRIG:3;
A5: now :: thesis: not Re r = 1
assume A6: Re r = 1 ; :: thesis: contradiction
then Im r = 0 by A4;
hence contradiction by A3, A6, COMPLEX1:13; :: thesis: verum
end;
Re r <= 1 by A2, COMPLEX1:54;
then Re r < 1 by A5, XXREAL_0:1;
then 2 * q > (2 * q) * (Re r) by A1, XREAL_1:157;
then - ((2 * q) * (Re r)) > - (2 * q) by XREAL_1:24;
then (- (2 * q)) + (q ^2) < (- ((2 * q) * (Re r))) + (q ^2) by XREAL_1:8;
then A7: ((q ^2) - ((2 * q) * (Re r))) + 1 > ((q ^2) - (2 * q)) + 1 by XREAL_1:8;
reconsider qc = [**q,0**] as Element of F_Complex ;
A8: ( Re [**(q - (Re r)),(- (Im r))**] = q - (Re r) & Im [**(q - (Re r)),(- (Im r))**] = - (Im r) ) by COMPLEX1:12;
|.(qc - r).| ^2 = |.([**q,0**] - [**(Re r),(Im r)**]).| ^2 by COMPLEX1:13
.= |.[**(q - (Re r)),(0 - (Im r))**].| ^2 by POLYNOM5:6
.= ((q - (Re r)) ^2) + ((Im r) ^2) by A8, COMPTRIG:3
.= ((q ^2) - ((2 * q) * (Re r))) + 1 by A4 ;
then ( |.(qc - r).| >= 0 & |.(qc - r).| ^2 > (q - 1) ^2 ) by A7, COMPLEX1:46;
hence |.([**q,0**] - r).| > q - 1 by SQUARE_1:48; :: thesis: verum