let z1, z2, z3, z be Element of COMPLEX ; :: thesis: ( z1 <> 0 & Polynom z1,z2,z3,z = 0 implies for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t holds
z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t )
assume A1: ( z1 <> 0 & Polynom z1,z2,z3,z = 0 ) ; :: thesis: for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t holds
z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t
let h, t be Element of COMPLEX ; :: thesis: ( h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t implies z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t )
assume A2: ( h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) ) ; :: thesis: ( z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t )
(((z1 * (z ^2 )) + (z2 * z)) + z3) / z1 = 0 by A1;
then ((((z ^2 ) * z1) / z1) + ((z2 * z) / z1)) + (z3 / z1) = 0 ;
then ((z ^2 ) + ((z2 / z1) * z)) + (z3 / z1) = 0 by A1, XCMPLX_1:90;
then ((z ^2 ) + (((2 * z2) / (2 * z1)) * z)) + (z3 / z1) = 0 by XCMPLX_1:92;
then ((z + (z2 / (2 * z1))) ^2 ) - (((z2 / (2 * z1)) ^2 ) - (z3 / z1)) = 0 ;
then ( (z + t) - t = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t or (z + t) - t = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or (z + t) - t = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or (z + t) - t = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t ) by A2, Th32;
hence ( z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) * <i> )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2 ) + ((Im h) ^2 )))) / 2)) * <i> )) - t ) ; :: thesis: verum