let z, s be Element of COMPLEX ; :: thesis: ( 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 ; :: thesis: ( 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> ) )
assume A2: Im s >= 0 ; :: thesis: ( 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 a = Re s;
set b = Im s;
set u = Re z;
set v = Im z;
z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
then B4: (((Re z) ^2 ) - ((Im z) ^2 )) + (((2 * (Re z)) * (Im z)) * <i> ) = (Re s) + ((Im s) * <i> ) by A1, COMPLEX1:29;
then A4: ( ((Re z) ^2 ) - ((Im z) ^2 ) = Re s & (2 * (Re z)) * (Im z) = Im s ) by COMPLEX1:163;
then A5: (((Re z) ^2 ) + ((Im z) ^2 )) ^2 = ((Re s) ^2 ) + ((Im s) ^2 ) ;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:65;
then A6: ((Re z) ^2 ) + ((Im z) ^2 ) = sqrt (((Re s) ^2 ) + ((Im s) ^2 )) by A5, SQUARE_1:89;
( ( Re z <= 0 & Im z <= 0 ) or ( Re z >= 0 & Im z >= 0 ) ) by A2, B4, COMPLEX1:163;
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 A4, A6, 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; :: thesis: verum