let z, z1, z2, z3 be Complex; :: thesis: ( z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 implies for s, h, t being 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 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 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, Th26; :: thesis: verum