let z1, z3, z be Element of COMPLEX ; :: thesis: ( z1 <> 0 & Polynom z1,0 ,z3,z = 0 implies for s being Element of COMPLEX holds
( not s = - (z3 / z1) 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> ) 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 A1: ( z1 <> 0 & Polynom z1,0 ,z3,z = 0 ) ; :: thesis: for s being Element of COMPLEX holds
( not s = - (z3 / z1) 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> ) 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> ) )
let s be Element of COMPLEX ; :: thesis: ( not s = - (z3 / z1) 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> ) 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: s = - (z3 / z1) ; :: 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> ) 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> ) )
z ^2 = (- z3) / z1 by A1, XCMPLX_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> ) 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> ) ) by A2, Th32; :: thesis: verum