:: deftheorem Def2 defines 1_root_of_cubic POLYEQ_5:def 2 :
for a0, a1, a2, b₄ being Complex holds
( ( (3 * a1) - (a2 |^ 2) = 0 implies ( b₄ = 1_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 - (a2 / 3) ) ) ) & ( not (3 * a1) - (a2 |^ 2) = 0 implies ( b₄ = 1_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) - (a2 / 3) ) ) ) );