theorem Th21: :: POLYEQ_5:21

for z, a0, a1, a2, a3, x, q, r, p being Complex st z = x - (a3 / 4) & p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 holds
( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((x |^ 4) + ((4 * p) * (x |^ 2))) + ((8 * q) * x)) + (4 * r) = 0 )