let x, xv be Element of COMPLEX ; :: thesis: for u, v, uv, vv being Element of REAL st x = u + (v * <i> ) & xv = uv + (vv * <i> ) & uv < 0 holds
( ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) )
let u, v, uv, vv be Element of REAL ; :: thesis: ( x = u + (v * <i> ) & xv = uv + (vv * <i> ) & uv < 0 implies ( ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) ) )
assume A1: ( x = u + (v * <i> ) & xv = uv + (vv * <i> ) & uv < 0 ) ; :: thesis: ( ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) )

now

assume u < 0 ; :: thesis: |.(x + (xv *' )).| > |.(x - xv).|
then u * uv > 0 * uv by A1;
then 4 * (u * uv) > 4 * 0 ;
then (4 * u) * uv > 0 ;
then (|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) > 0 by A1, Lm14;
then A2: ((|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 )) + (|.(x - xv).| ^2 ) > 0 + (|.(x - xv).| ^2 ) by XREAL_1:8;
( 0 <= |.(x + (xv *' )).| & 0 <= |.(x - xv).| ) by COMPLEX1:132;
hence |.(x + (xv *' )).| > |.(x - xv).| by A2, XREAL_1:68; :: thesis: verum

end;

hence ( u < 0 implies |.(x - xv).| < |.(x + (xv *' )).| ) ; :: thesis: ( ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) )

now

assume u > 0 ; :: thesis: |.(x + (xv *' )).| < |.(x - xv).|
then u * uv < 0 * uv by A1;
then 4 * (u * uv) < 4 * 0 ;
then (4 * u) * uv < 0 ;
then (|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) < 0 by A1, Lm14;
then A3: ((|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 )) + (|.(x - xv).| ^2 ) < 0 + (|.(x - xv).| ^2 ) by XREAL_1:8;
( 0 <= |.(x + (xv *' )).| & 0 <= |.(x - xv).| ) by COMPLEX1:132;
hence |.(x + (xv *' )).| < |.(x - xv).| by A3, XREAL_1:68; :: thesis: verum

end;

hence ( u > 0 implies |.(x - xv).| > |.(x + (xv *' )).| ) ; :: thesis: ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| )

now

assume u = 0 ; :: thesis: |.(x - xv).| = |.(x + (xv *' )).|
then (4 * u) * uv = 0 ;
then A4: (|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = 0 by A1, Lm14;

now

assume A5: |.(x - xv).| <> |.(x + (xv *' )).| ; :: thesis: contradiction

per cases ( |.(x - xv).| > |.(x + (xv *' )).| or |.(x - xv).| < |.(x + (xv *' )).| ) by A5, XXREAL_0:1;

suppose |.(x - xv).| > |.(x + (xv *' )).| ; :: thesis: contradiction

hence contradiction by A4, COMPLEX1:132, SQUARE_1:78; :: thesis: verum

end;

suppose |.(x - xv).| < |.(x + (xv *' )).| ; :: thesis: contradiction

hence contradiction by A4, COMPLEX1:132, SQUARE_1:78; :: thesis: verum

end;

end;

end;

hence |.(x - xv).| = |.(x + (xv *' )).| ; :: thesis: verum

end;

hence ( u = 0 implies |.(x - xv).| = |.(x + (xv *' )).| ) ; :: thesis: verum