let a0, a1, a2 be Complex; (((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) = a1
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))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) = a1set r =
((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54;
set s1 = 3
-root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54));
A2:
( 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;
thus (((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) =
((1_root_of_cubic (a0,a1,a2)) * ((2_root_of_cubic (a0,a1,a2)) + (3_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)))) + ((((- ((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, A2, Def2
.=
((((- (((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)))) / 4)) - ((a2 * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) / 3)) + (((3 * a2) * a2) / 9)) + ((a2 * (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)))) / 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 -root 3) * (2 -root 3))) * (- 1)) / 2) / 2)
.=
((- (((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)))) / 4)) + ((a2 * a2) / 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 -root 3) |^ 2)) * (- 1)) / 2) / 2)
by Th1
.=
((- (((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)))) / 4)) + ((a2 * a2) / 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)))) * 3) * (- 1)) / 2) / 2)
by Th7
.=
(a2 |^ 2) / 3
by Th1
.=
a1
by A1
;
verum end; suppose A3:
(3 * a1) - (a2 |^ 2) <> 0
;
(((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) = a1set 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))))));
A4:
3
-root ((((((9 * a2) * a1) - (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
A6:
( 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 A3, Def3, Def4;
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)))))));
thus (((1_root_of_cubic (a0,a1,a2)) * (2_root_of_cubic (a0,a1,a2))) + ((1_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2)))) + ((2_root_of_cubic (a0,a1,a2)) * (3_root_of_cubic (a0,a1,a2))) =
((1_root_of_cubic (a0,a1,a2)) * ((2_root_of_cubic (a0,a1,a2)) + (3_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)))) + ((((- (((3 -root ((((((9 * a2) * a1) - (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 A3, A6, Def2
.=
((((- (((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))))))))) / 4)) - ((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))))))))) / 3)) + (((3 * a2) * a2) / 9)) + ((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))))))))) / 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 -root 3) * (2 -root 3))) * (- 1)) / 4)
.=
((- (((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))))))))) / 4)) + ((a2 * 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)))))))) * ((3 -root ((((((9 * a2) * a1) - (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) |^ 2)) * (- 1)) / 4)
by Th1
.=
((- (((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))))))))) / 4)) + ((a2 * 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)))))))) * ((3 -root ((((((9 * a2) * a1) - (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) * (- 1)) / 4)
by Th7
.=
((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))))))) + ((a2 * a2) / 3)
.=
(3 * (((3 * a1) - (a2 |^ 2)) / 9)) + ((a2 * a2) / 3)
by A4, XCMPLX_1:90
.=
(3 * (((3 * a1) - (a2 |^ 2)) / 9)) + ((a2 |^ 2) / 3)
by Th1
.=
a1
;
verum end; end;