theorem :: POLYEQ_3:14

for a, c, d being Real
for z being Complex st a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 holds
for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>)