let z, z1, z3 be Complex; :: thesis: ( z1 <> 0 & Polynom (z1,0,z3,z) = 0 implies for s being 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 ( z1 <> 0 & Polynom (z1,0,z3,z) = 0 ) ; :: thesis: for s being 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>) )
then A1: z ^2 = (- z3) / z1 by XCMPLX_1:89;
let s be 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 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>) )
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 A1, Th23; :: thesis: verum