let a0, a1, a2, a3 be Complex; :: thesis: (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3

per cases ( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 or ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0 ) ;

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

then A2: ( 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) & 3_root_of_quartic (a0,a1,a2,a3) = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) & 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) & 4_root_of_quartic (a0,a1,a2,a3) = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) ) ) by Def7, Def8;
( 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) & 1_root_of_quartic (a0,a1,a2,a3) = (2 -root (- (2 * (p - s1)))) - (a3 / 4) ) & 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) & 2_root_of_quartic (a0,a1,a2,a3) = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) ) ) by A1, Def5, Def6;
hence (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3 by A2; :: thesis: verum

end;

suppose A3: ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0 ; :: thesis: (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3

then A4: ( 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)) & 3_root_of_quartic (a0,a1,a2,a3) = (((- s1) + s2) - s3) - (a3 / 4) ) & 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)) & 4_root_of_quartic (a0,a1,a2,a3) = ((s1 - s2) - s3) - (a3 / 4) ) ) by Def7, Def8;
( 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)) & 1_root_of_quartic (a0,a1,a2,a3) = ((s1 + s2) + s3) - (a3 / 4) ) & 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)) & 2_root_of_quartic (a0,a1,a2,a3) = (((- s1) - s2) + s3) - (a3 / 4) ) ) by A3, Def5, Def6;
hence (((1_root_of_quartic (a0,a1,a2,a3)) + (2_root_of_quartic (a0,a1,a2,a3))) + (3_root_of_quartic (a0,a1,a2,a3))) + (4_root_of_quartic (a0,a1,a2,a3)) = - a3 by A4; :: thesis: verum

end;

end;