let z1, z2, z3, z be Element of COMPLEX ; :: thesis: ( z1 <> 0 & Polynom z1,z2,z3,0 ,z = 0 implies for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & 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 that
A1: z1 <> 0 and
A2: Polynom z1,z2,z3,0 ,z = 0 ; :: thesis: for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & 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 s, h, t be Element of COMPLEX ; :: thesis: ( h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & 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 )
0 = (Polynom z1,z2,z3,z) * z by A2;
then A3: ( z = 0 or Polynom z1,z2,z3,z = 0 ) ;
assume ( h = ((z2 / (2 * z1)) ^2 ) - (z3 / z1) & t = z2 / (2 * z1) ) ; :: thesis: ( z = 0 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 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 )
hence ( z = 0 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 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 ) by A1, A3, Th37; :: thesis: verum