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 that
A1: x = u + (v * <i>) and
A2: xv = uv + (vv * <i>) and
A3: 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 :: thesis: ( u < 0 implies |.(x + (xv *')).| > |.(x - xv).| )
assume u < 0 ; :: thesis: |.(x + (xv *')).| > |.(x - xv).|
then (4 * u) * uv > 0 by A3;
then (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) > 0 by A1, A2, Lm13;
then A4: ((|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2)) + (|.(x - xv).| ^2) > 0 + (|.(x - xv).| ^2) by XREAL_1:6;
0 <= |.(x + (xv *')).| by COMPLEX1:46;
hence |.(x + (xv *')).| > |.(x - xv).| by A4, XREAL_1:66; :: 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 :: thesis: ( u > 0 implies |.(x + (xv *')).| < |.(x - xv).| )
assume u > 0 ; :: thesis: |.(x + (xv *')).| < |.(x - xv).|
then (4 * u) * uv < 0 by A3;
then (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) < 0 by A1, A2, Lm13;
then A5: ((|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2)) + (|.(x - xv).| ^2) < 0 + (|.(x - xv).| ^2) by XREAL_1:6;
0 <= |.(x - xv).| by COMPLEX1:46;
hence |.(x + (xv *')).| < |.(x - xv).| by A5, XREAL_1:66; :: thesis: verum
end;
hence ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) ; :: thesis: ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| )
now :: thesis: ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| )
assume u = 0 ; :: thesis: |.(x - xv).| = |.(x + (xv *')).|
then (4 * u) * uv = 0 ;
then A6: (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = 0 by A1, A2, Lm13;
now :: thesis: not |.(x - xv).| <> |.(x + (xv *')).|
assume A7: |.(x - xv).| <> |.(x + (xv *')).| ; :: thesis: contradiction
per cases ( |.(x - xv).| > |.(x + (xv *')).| or |.(x - xv).| < |.(x + (xv *')).| ) by A7, XXREAL_0:1;
end;
end;
hence |.(x - xv).| = |.(x + (xv *')).| ; :: thesis: verum
end;
hence ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) ; :: thesis: verum