let a, b, c, d be Real; :: thesis: for z being Element of COMPLEX st a <> 0 & Polynom a,b,c,d,z = 0 & Im z = 0 holds
for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> )
let z be Element of COMPLEX ; :: thesis: ( a <> 0 & Polynom a,b,c,d,z = 0 & Im z = 0 implies for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
assume A1: a <> 0 ; :: thesis: ( not Polynom a,b,c,d,z = 0 or not Im z = 0 or for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
assume A2: ( Polynom a,b,c,d,z = 0 & Im z = 0 ) ; :: thesis: for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> )
let u, v, x1 be Real; :: thesis: ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) implies z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
assume A3: ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) = 0 ) ; :: thesis: ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) )
set x = Re z;
set y = Im z;
A6: a = a + (0 * <i> ) ;
A7: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
0 = (((a * ((Re (z ^3 )) + ((Im (z ^3 )) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d by A2, COMPLEX1:29
.= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + ((Im (z ^3 )) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d by Th11
.= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) + (b * (z ^2 ))) + (c * z)) + d by Th11
.= ((((a + (0 * <i> )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by COMPLEX1:29
.= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * (Im a))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by COMPLEX1:def 10
.= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - (0 * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * (Im a))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by A6, COMPLEX1:28
.= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - 0 ) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) * 0 )) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by A6, COMPLEX1:28
.= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> )))) - 0 ) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + 0 ) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by COMPLEX1:28
.= ((((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by COMPLEX1:28
.= (((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) - 0 ) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * (z ^2 ))) + (c * ((Re z) + ((Im z) * <i> )))) + d by A6, COMPLEX1:28
.= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 )))) + ((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) * <i> )) + (b * ((((Re z) ^2 ) - ((Im z) ^2 )) + (((2 * (Re z)) * (Im z)) * <i> )))) + ((c * (Re z)) + ((c * (Im z)) * <i> ))) + d by A7, A6, COMPLEX1:28 ;
then 0 = ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * 0 ))) + (b * (((Re z) ^2 ) - 0 ))) + (c * (Re z))) + d) + ((((a * ((- (0 |^ 3)) + 0 )) + (b * 0 )) + 0 ) * <i> ) by A2
.= ((((a * ((Re z) |^ 3)) + (b * ((Re z) ^2 ))) + (c * (Re z))) + d) + (((a * 0 ) + 0 ) * <i> ) by NEWTON:16 ;
then A8: Polynom a,b,c,d,(Re z) = 0 ;
set a' = b / a;
set b' = c / a;
set c' = d / a;
set h = - (b / (3 * a));
A9: ( b / a = b / a & c / a = c / a & d / a = d / a & - (b / (3 * a)) = - (b / (3 * a)) ) ;
set p = (((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ));
set q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )));
((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3 = (1 / 3) * ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) ;
then A10: ((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3 = (((3 * a) * c) - (b ^2 )) / (((a ^2 ) * 3) * 3) by XCMPLX_1:104;
A11: - (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2) = - (((b / (3 * a)) |^ 3) + ((1 / 2) * ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))))
.= - (((b / (3 * a)) |^ 3) + ((((3 * a) * d) - (b * c)) / (((a ^2 ) * 3) * 2))) by XCMPLX_1:104
.= (- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 ))) ;
Polynom 1,0 ,((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))),((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))),x1 = 0 by A1, A3, A8, A9, POLYEQ_1:16;
then ( x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + ((((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) / 3) |^ 3))))) ) by A3, POLYEQ_1:19;
hence ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2 )))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) ^2 ) / 4) + (((((3 * a) * c) - (b ^2 )) / (9 * (a ^2 ))) |^ 3)))))) - (b / (3 * a))) + (0 * <i> ) ) by A2, A3, A10, A11, COMPLEX1:29; :: thesis: verum