let z, s be Element of COMPLEX ; :: thesis: ( z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * <i> implies z = - ((sqrt (- (Re s))) * <i> ) )
assume A1: z ^2 = s ; :: thesis: ( not Im s = 0 or not Re s < 0 or z = (sqrt (- (Re s))) * <i> or z = - ((sqrt (- (Re s))) * <i> ) )
assume that
A2: Im s = 0 and
A3: Re s < 0 ; :: thesis: ( z = (sqrt (- (Re s))) * <i> or z = - ((sqrt (- (Re s))) * <i> ) )
( z = (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + 0 ))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + 0 ))) / 2)) * <i> ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + 0 ))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + (0 ^2 )))) / 2))) * <i> ) ) by A1, A2, Th28;
then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + 0 ))) / 2)) * <i> ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2 ) + 0 ))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + 0 ))) / 2))) * <i> ) ) by A3, SQUARE_1:90;
then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (- (Re s))) / 2)) * <i> ) or z = (- (sqrt (((Re s) + (- (Re s))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2 ) + 0 ))) / 2))) * <i> ) ) by A3, SQUARE_1:90;
then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (- (Re s))) / 2)) * <i> ) or z = (- (sqrt (((Re s) + (- (Re s))) / 2))) + ((- (sqrt (((- (Re s)) + (- (Re s))) / 2))) * <i> ) ) by A3, SQUARE_1:90;
hence ( z = (sqrt (- (Re s))) * <i> or z = - ((sqrt (- (Re s))) * <i> ) ) by SQUARE_1:82; :: thesis: verum