:: deftheorem Def4 defines 3_root_of_cubic POLYEQ_5:def 4 :
for a0, a1, a2, b₄ being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b₄ = 3_root_of_cubic (a0,a1,a2) iff ex r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & b₄ = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i>) / 2) ) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ( b₄ = 3_root_of_cubic (a0,a1,a2) iff ex q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b₄ = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) ) );