let z, s be Element of COMPLEX ; ( z ^2 = s & Im s < 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) * <i> ) implies z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) * <i> ) )
assume A1:
z ^2 = s
; ( not Im s < 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) * <i> ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) * <i> ) )
set v = Im z;
set u = Re z;
set b = Im s;
set a = Re s;
z = (Re z) + ((Im z) * <i> )
by COMPLEX1:29;
then A2:
( s = (Re s) + ((Im s) * <i> ) & z ^2 = (((Re z) ^2 ) - ((Im z) ^2 )) + (((2 * (Re z)) * (Im z)) * <i> ) )
by COMPLEX1:29;
assume
Im s < 0
; ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) * <i> ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) * <i> ) )
then
2 * ((Re z) * (Im z)) < 0
by A1, A2, COMPLEX1:163;
then
(Re z) * (Im z) < 0
;
then A3:
( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) )
by XREAL_1:135;
A4:
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 )
by XREAL_1:65;
A5:
((Re z) ^2 ) - ((Im z) ^2 ) = Re s
by A1, A2, COMPLEX1:163;
then
sqrt ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 ) = sqrt (((Re s) ^2 ) + ((Im s) ^2 ))
by A1, A2;
then
((Re z) ^2 ) + ((Im z) ^2 ) = sqrt (((Re s) ^2 ) + ((Im s) ^2 ))
by A4, SQUARE_1:89;
then
( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2) ) )
by A5, A3, SQUARE_1:89, SQUARE_1:90;
hence
( z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) * <i> ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + ((Im s) ^2 )))) / 2)) * <i> ) )
by COMPLEX1:29; verum