let s, z be 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:13;
then A2:
( s = (Re s) + ((Im s) * <i>) & z ^2 = (((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>) )
by COMPLEX1:13;
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:77;
then
(Re z) * (Im z) < 0
;
then A3:
( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) )
by XREAL_1:133;
A4:
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 )
by XREAL_1:63;
A5:
((Re z) ^2) - ((Im z) ^2) = Re s
by A1, A2, COMPLEX1:77;
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:22;
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:22, SQUARE_1:23;
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:13; verum