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> ) holds
(|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = (4 * u) * uv
let u, v, uv, vv be Element of REAL ; :: thesis: ( 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> ) ; :: thesis: (|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = (4 * u) * uv
A3: (u + uv) ^2 >= 0 by XREAL_1:65;
A4: (v + (- vv)) ^2 >= 0 by XREAL_1:65;
|.(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:28
.= sqrt (((u + (Re xv)) ^2 ) + ((Im (x + (xv *' ))) ^2 )) by COMPLEX1:112
.= sqrt (((u + uv) ^2 ) + ((Im (x + (xv *' ))) ^2 )) by A2, COMPLEX1:28
.= sqrt (((u + uv) ^2 ) + (((Im x) + (Im (xv *' ))) ^2 )) by COMPLEX1:19
.= sqrt (((u + uv) ^2 ) + ((v + (Im (xv *' ))) ^2 )) by A1, COMPLEX1:28
.= sqrt (((u + uv) ^2 ) + ((v + (- (Im xv))) ^2 )) by COMPLEX1:112
.= sqrt (((u + uv) ^2 ) + ((v + (- vv)) ^2 )) by A2, COMPLEX1:28 ;
then A5: |.(x + (xv *' )).| ^2 = ((u + uv) ^2 ) + ((v + (- vv)) ^2 ) by A3, A4, SQUARE_1:def 4;
A6: (u - uv) ^2 >= 0 by XREAL_1:65;
A7: (((u + uv) ^2 ) + ((v + (- vv)) ^2 )) - (((u - uv) ^2 ) + ((v - vv) ^2 )) = (4 * u) * uv ;
A8: (v - vv) ^2 >= 0 by XREAL_1:65;
|.(x - xv).| = sqrt ((((Re x) - (Re xv)) ^2 ) + ((Im (x - xv)) ^2 )) by COMPLEX1:48
.= sqrt (((u - (Re xv)) ^2 ) + ((Im (x - xv)) ^2 )) by A1, COMPLEX1:28
.= sqrt (((u - uv) ^2 ) + ((Im (x - xv)) ^2 )) by A2, COMPLEX1:28
.= sqrt (((u - uv) ^2 ) + (((Im x) - (Im xv)) ^2 )) by COMPLEX1:48
.= sqrt (((u - uv) ^2 ) + ((v - (Im xv)) ^2 )) by A1, COMPLEX1:28
.= sqrt (((u - uv) ^2 ) + ((v - vv) ^2 )) by A2, COMPLEX1:28 ;
hence (|.(x + (xv *' )).| ^2 ) - (|.(x - xv).| ^2 ) = (4 * u) * uv by A5, A6, A8, A7, SQUARE_1:def 4; :: thesis: verum