let a0, a1, a2 be Complex; ((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
;
((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) * (3_root_of_cubic (a0,a1,a2)) = - a0set 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
;
verum end; suppose A2:
(3 * a1) - (a2 |^ 2) <> 0
;
((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) * (3_root_of_cubic (a0,a1,a2)) = - a0set 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
;
verum end;