let a0, a1, a2 be complex number ; :: thesis: ((1_root_of_cubic a0,a1,a2) + (2_root_of_cubic a0,a1,a2)) + (3_root_of_cubic a0,a1,a2) = - a2

per cases ( (3 * a1) - (a2 |^ 2) = 0 or (3 * a1) - (a2 |^ 2) <> 0 ) ;

suppose A1: (3 * a1) - (a2 |^ 2) = 0 ; :: thesis: ((1_root_of_cubic a0,a1,a2) + (2_root_of_cubic a0,a1,a2)) + (3_root_of_cubic a0,a1,a2) = - a2

A2: ex r, s1 being complex number st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 1_root_of_cubic a0,a1,a2 = s1 - (a2 / 3) ) by A1, Def2;
A3: ex r, s1 being complex number st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 2_root_of_cubic a0,a1,a2 = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) ) by A1, Def3;
ex r, s1 being complex number st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & 3_root_of_cubic a0,a1,a2 = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) by A1, Def4;
hence ((1_root_of_cubic a0,a1,a2) + (2_root_of_cubic a0,a1,a2)) + (3_root_of_cubic a0,a1,a2) = - a2 by A2, A3; :: thesis: verum

end;

suppose A5: (3 * a1) - (a2 |^ 2) <> 0 ; :: thesis: ((1_root_of_cubic a0,a1,a2) + (2_root_of_cubic a0,a1,a2)) + (3_root_of_cubic a0,a1,a2) = - a2

A6: ex q, r, s, s1, s2 being complex number 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) & 1_root_of_cubic a0,a1,a2 = (s1 + s2) - (a2 / 3) ) by A5, Def2;
A7: ex q, r, s, s1, s2 being complex number 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) & 2_root_of_cubic a0,a1,a2 = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i> ) / 2) ) by A5, Def3;
ex q, r, s, s1, s2 being complex number 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) & 3_root_of_cubic a0,a1,a2 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i> ) / 2) ) by A5, Def4;
hence ((1_root_of_cubic a0,a1,a2) + (2_root_of_cubic a0,a1,a2)) + (3_root_of_cubic a0,a1,a2) = - a2 by A6, A7; :: thesis: verum

end;

end;