theorem :: POLYEQ_5:15

for z, a0, a1, a2, s1, s2, q, r, s being Complex st q = ((3 * a1) - (a2 |^ 2)) / 9 & q <> 0 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) holds
( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) )