theorem Th13: :: POLYEQ_5:13

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