theorem Th23: :: POLYEQ_5:23

for z, s1, s2, q, r, s3, p being Complex st q <> 0 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) holds
( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) )