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) = - a0

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) = - a0

A2: 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;
A3: 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;
set r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54;
set s1 = 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54));
thus ((1_root_of_cubic a0,a1,a2) * (2_root_of_cubic a0,a1,a2)) * (3_root_of_cubic a0,a1,a2) = (((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3)) * (((- ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2)) - (a2 / 3)) + ((((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) * (2 -root 3)) * <i> ) / 2))) * (((- ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2)) - (a2 / 3)) - ((((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) * (2 -root 3)) * <i> ) / 2)) by A1, Def2, A2, A3
.= ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3)) * (((((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3)) * (((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3))) + ((((((2 -root 3) * (2 -root 3)) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) / 2) / 2))
.= ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3)) * (((((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3)) * (((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3))) + ((((((2 -root 3) |^ 2) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) / 2) / 2)) by Th1
.= ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3)) * (((((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3)) * (((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / 2) + (a2 / 3))) + ((((3 * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) / 2) / 2)) by Th8
.= (((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) - (((((a2 * a2) * a2) / 3) / 3) / 3)
.= ((3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) |^ 3) - (((a2 * a2) * a2) / 27) by Th2
.= (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) - (((a2 * a2) * a2) / 27) by Th8
.= (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 27) - ((a2 |^ 3) / 27) by Th2
.= ((((3 * a2) * a1) - (a2 |^ (2 + 1))) / 9) - a0
.= ((((3 * a2) * a1) - ((a2 |^ 2) * a2)) / 9) - a0 by NEWTON:11
.= - a0 by A1 ; :: thesis: verum

end;

suppose A4: (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) = - a0

A5: 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 A4, Def3;
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) & 3_root_of_cubic a0,a1,a2 = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i> ) / 2) ) by A4, Def4;
set q = ((3 * a1) - (a2 |^ 2)) / 9;
set r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54;
set s = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2));
set s1 = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))));
set s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))));
set t = (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))));
set d = (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))));
A7: ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) = (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3 by Th2
.= (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) by Th8 ;
A8: 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) <> 0

proof

assume A9: 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) = 0 ; :: thesis: contradiction
A10: 0 = (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3 by A9, NEWTON:16
.= (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) by Th8 ;
((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2) = (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) |^ 2 by Th8
.= (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) by Th1
.= (- (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) * (- (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))
.= (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2 by A10, Th1 ;
then ((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9) = 0 by Th2;
hence contradiction by A4; :: thesis: verum

end;

A11: (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) = - (((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))
.= - (((3 * a1) - (a2 |^ 2)) / 9) by A8, XCMPLX_1:88 ;
A12: ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) = ((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) * ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) by A7, A8, XCMPLX_1:90
.= ((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) * ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9))) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) by XCMPLX_1:121
.= (((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) + ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + ((2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - ((((3 * a1) - (a2 |^ 2)) / 9) |^ 3)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) by Th2
.= (((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) + ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + ((2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) |^ 2)) - ((((3 * a1) - (a2 |^ 2)) / 9) |^ 3)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) by Th1
.= (((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) + ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))) - ((((3 * a1) - (a2 |^ 2)) / 9) |^ 3)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) by Th8
.= ((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) + ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))
.= ((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) + ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) by Th1
.= ((2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) * ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))
.= 2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) by A7, A8, XCMPLX_1:90 ;
thus ((1_root_of_cubic a0,a1,a2) * (2_root_of_cubic a0,a1,a2)) * (3_root_of_cubic a0,a1,a2) = ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3)) * (((- (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2)) - (a2 / 3)) + (((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) * (2 -root 3)) * <i> ) / 2))) * (((- (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2)) - (a2 / 3)) - (((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) * (2 -root 3)) * <i> ) / 2)) by A4, Def2, A5, A6
.= (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3)) * ((((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3)) * ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3))) + ((((((2 -root 3) * (2 -root 3)) * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) / 2) / 2))
.= (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3)) * ((((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3)) * ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3))) + ((((((2 -root 3) |^ 2) * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) / 2) / 2)) by Th1
.= (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3)) * ((((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3)) * ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) / 2) + (a2 / 3))) + ((((3 * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) - (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) / 2) / 2)) by Th8
.= (((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) + (((- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) + ((a2 * ((4 * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) / 4)) - (((a2 * a2) * a2) / 27)
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) + (((- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) + (a2 * ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))))) - (((a2 * a2) * a2) / 27) by Th2
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) + (((- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) * (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))))) + (a2 * (- (((3 * a1) - (a2 |^ 2)) / 9)))) - (((a2 * a2) * a2) / 27) by A11
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) - ((((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) * ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27)
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))))) * ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27) by XCMPLX_1:77
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / (((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) * (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27) by XCMPLX_1:77
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27) by Th2
.= ((((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) |^ 3) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27) by Th8
.= ((((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) - ((((((3 * a1) - (a2 |^ 2)) / 9) * (((3 * a1) - (a2 |^ 2)) / 9)) * (((3 * a1) - (a2 |^ 2)) / 9)) / ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - (((a2 * a2) * a2) / 27) by Th8
.= (((2 * ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0))) / 54) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - ((a2 |^ 3) / 27) by A12, Th2
.= (((((9 * a2) * a1) - (3 * (a2 |^ 3))) / 27) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - a0
.= (((((9 * a2) * a1) - (3 * ((a2 * a2) * a2))) / 27) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - a0 by Th2
.= (((a2 * ((3 * a1) - (a2 * a2))) / 9) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - a0
.= (((a2 * ((3 * a1) - (a2 |^ 2))) / 9) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - a0 by Th1
.= - a0 ; :: thesis: verum

end;

end;