:: deftheorem Def5 defines 1_root_of_quartic POLYEQ_5:def 5 :
for a0, a1, a2, a3, b₅ being Complex holds
( ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b₅ = 1_root_of_quartic (a0,a1,a2,a3) iff ex p, r, s1 being Complex st
( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root ((p |^ 2) - r) & b₅ = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) ) ) & ( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ( b₅ = 1_root_of_quartic (a0,a1,a2,a3) iff ex p, q, r, s1, s2, s3 being Complex st
( 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 & 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)) & b₅ = ((s1 + s2) + s3) - (a3 / 4) ) ) ) );