let x, xv be Element of COMPLEX ; for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) holds
(|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv
let u, v, uv, vv be Element of REAL ; ( x = u + (v * <i>) & xv = uv + (vv * <i>) implies (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv )
assume that
A1:
x = u + (v * <i>)
and
A2:
xv = uv + (vv * <i>)
; (|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv
A3:
(u + uv) ^2 >= 0
by XREAL_1:63;
A4:
(v + (- vv)) ^2 >= 0
by XREAL_1:63;
|.(x + (xv *')).| =
sqrt ((((Re x) + (Re (xv *'))) ^2) + ((Im (x + (xv *'))) ^2))
by COMPLEX1:8
.=
sqrt (((u + (Re (xv *'))) ^2) + ((Im (x + (xv *'))) ^2))
by A1, COMPLEX1:12
.=
sqrt (((u + (Re xv)) ^2) + ((Im (x + (xv *'))) ^2))
by COMPLEX1:27
.=
sqrt (((u + uv) ^2) + ((Im (x + (xv *'))) ^2))
by A2, COMPLEX1:12
.=
sqrt (((u + uv) ^2) + (((Im x) + (Im (xv *'))) ^2))
by COMPLEX1:8
.=
sqrt (((u + uv) ^2) + ((v + (Im (xv *'))) ^2))
by A1, COMPLEX1:12
.=
sqrt (((u + uv) ^2) + ((v + (- (Im xv))) ^2))
by COMPLEX1:27
.=
sqrt (((u + uv) ^2) + ((v + (- vv)) ^2))
by A2, COMPLEX1:12
;
then A5:
|.(x + (xv *')).| ^2 = ((u + uv) ^2) + ((v + (- vv)) ^2)
by A3, A4, SQUARE_1:def 2;
A6:
(u - uv) ^2 >= 0
by XREAL_1:63;
A7:
(((u + uv) ^2) + ((v + (- vv)) ^2)) - (((u - uv) ^2) + ((v - vv) ^2)) = (4 * u) * uv
;
A8:
(v - vv) ^2 >= 0
by XREAL_1:63;
|.(x - xv).| =
sqrt ((((Re x) - (Re xv)) ^2) + ((Im (x - xv)) ^2))
by COMPLEX1:19
.=
sqrt (((u - (Re xv)) ^2) + ((Im (x - xv)) ^2))
by A1, COMPLEX1:12
.=
sqrt (((u - uv) ^2) + ((Im (x - xv)) ^2))
by A2, COMPLEX1:12
.=
sqrt (((u - uv) ^2) + (((Im x) - (Im xv)) ^2))
by COMPLEX1:19
.=
sqrt (((u - uv) ^2) + ((v - (Im xv)) ^2))
by A1, COMPLEX1:12
.=
sqrt (((u - uv) ^2) + ((v - vv) ^2))
by A2, COMPLEX1:12
;
hence
(|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv
by A5, A6, A8, A7, SQUARE_1:def 2; verum