theorem :: POLYEQ_3:15

for a, b, c, d being Real
for z being 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>)