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