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;

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

|.([**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

Re r <= 1
by A2, COMPLEX1:54;assume A6:
Re r = 1
; :: thesis: contradiction

then Im r = 0 by A4;

hence contradiction by A3, A6, COMPLEX1:13; :: thesis: verum

end;then Im r = 0 by A4;

hence contradiction by A3, A6, COMPLEX1:13; :: thesis: verum

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