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))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_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))) = - a1

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))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_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))) = - a1

set p = ((8 * a2) - (3 * (a3 |^ 2))) / 32;
set r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024;
set s1 = 2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024));
set t1 = 2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))));
set t2 = 2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))));
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 A1, 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))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_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))) = (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) by A2
.= (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) by Th1
.= (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) by Th1
.= (((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) by Th7
.= (((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) by Th7
.= ((a2 - ((3 * (a3 |^ 2)) / 8)) + ((a3 * a3) / 8)) * (- (a3 / 2))
.= ((a2 - ((3 * (a3 * a3)) / 8)) + ((a3 * a3) / 8)) * (- (a3 / 2)) by Th1
.= (((a3 * a3) * a3) / 8) - ((a2 * a3) / 2)
.= ((a3 |^ 3) / 8) - (((4 * a2) * a3) / 8) by Th2
.= - a1 by A1 ;
:: 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))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_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))) = - a1

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;
set p = ((8 * a2) - (3 * (a3 |^ 2))) / 32;
set q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64;
set r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024;
set s1 = 2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))));
set s2 = 2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))));
set s3 = - (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))));
A5: (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) = (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) |^ 2 by Th1
.= 2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) by Th7 ;
A6: (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) = (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) |^ 2 by Th1
.= 1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) by Th7 ;
then A7: (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) * (3_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) = - (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)) by A5, Th19;
A8: ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) * ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) <> 0 by A3;
then A9: ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) <> 0 by A7, Th1;
((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) <> 0 by A8, A7, Th1;
then A10: (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) <> 0 ;
A11: (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) = ((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) by XCMPLX_1:187
.= ((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) * ((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) by XCMPLX_1:187
.= ((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) * (- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64))) / (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) by XCMPLX_1:76
.= (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) * ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))
.= ((3_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) / (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) by A7, Th1
.= 3_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) by A9, XCMPLX_1:89 ;
( 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))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (2_root_of_quartic (a0,a1,a2,a3))) * (4_root_of_quartic (a0,a1,a2,a3)))) + (((1_root_of_quartic (a0,a1,a2,a3)) * (3_root_of_quartic (a0,a1,a2,a3))) * (4_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))) = ((((((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) + ((2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) + ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))))) * a3) - (((a3 * a3) * a3) / 16)) + (((8 * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))) by A4
.= (((- (2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) * a3) - (((a3 * a3) * a3) / 16)) + (((8 * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))) by A6, A5, A11, Th17
.= (((- (((16 * a2) / 32) * a3)) + (((6 * (a3 |^ 2)) / 32) * a3)) - (((a3 * a3) * a3) / 16)) - (((8 * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))
.= (((- ((a2 / 2) * a3)) + (((6 * (a3 * a3)) / 32) * a3)) - (((a3 * a3) * a3) / 16)) - (((8 * (2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))) by Th1
.= ((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))))
.= ((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / (((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) / ((2 -root (1_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))) by XCMPLX_1:81
.= ((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / 1)) by A10, XCMPLX_1:60
.= ((- a1) + ((((2 * a3) * a3) * a3) / 16)) - ((8 * (a3 |^ 3)) / 64)
.= ((- a1) + ((((2 * a3) * a3) * a3) / 16)) - ((8 * ((a3 * a3) * a3)) / 64) by Th2
.= - a1 ;
:: thesis: verum

end;

end;