theorem :: POLYEQ_5:16

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