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));
( ex r, s1 being Complex 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) ) & ex r, s1 being Complex 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, Def3, Def4;
hence ((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
.= ((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 Th7
.= (((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 Th7
.= (((((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:6
.= - a0 by A1 ;
:: thesis: verum

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))))));
A3: 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 A5: ((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 Th7 ;
then A6: ((((((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 A3, XCMPLX_1:89
.= ((((((((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:120
.= (((((((((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 Th7
.= ((((((((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 A5, A3, XCMPLX_1:89 ;
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 * 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 A3, XCMPLX_1:87 ;
( 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) & 2_root_of_cubic (a0,a1,a2) = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) & 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) & 3_root_of_cubic (a0,a1,a2) = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) by A2, Def3, Def4;
hence ((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 A2, Def2
.= (((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 Th7
.= (((((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 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) - ((((((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:76
.= ((((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:76
.= ((((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 Th7
.= ((((((((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 Th7
.= (((2 * ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0))) / 54) - (a2 * (((3 * a1) - (a2 |^ 2)) / 9))) - ((a2 |^ 3) / 27) by A6, 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