let a0, a1, a2, a3 be complex number ; :: thesis: (((((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (3_root_of_quartic a0,a1,a2,a3)) + (((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((1_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((2_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3)) = - a1
per cases
( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 or ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0 )
;
suppose A1:
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0
;
:: thesis: (((((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (3_root_of_quartic a0,a1,a2,a3)) + (((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((1_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((2_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3)) = - a1A2:
ex
p,
r,
s1 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root ((p |^ 2) - r) &
1_root_of_quartic a0,
a1,
a2,
a3 = (2 -root (- (2 * (p - s1)))) - (a3 / 4) )
by A1, Def5;
A3:
ex
p,
r,
s1 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root ((p |^ 2) - r) &
2_root_of_quartic a0,
a1,
a2,
a3 = (- (2 -root (- (2 * (p - s1))))) - (a3 / 4) )
by A1, Def6;
A4:
ex
p,
r,
s1 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root ((p |^ 2) - r) &
3_root_of_quartic a0,
a1,
a2,
a3 = (2 -root (- (2 * (p + s1)))) - (a3 / 4) )
by A1, Def7;
A5:
ex
p,
r,
s1 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root ((p |^ 2) - r) &
4_root_of_quartic a0,
a1,
a2,
a3 = (- (2 -root (- (2 * (p + s1))))) - (a3 / 4) )
by A1, Def8;
set p =
((8 * a2) - (3 * (a3 |^ 2))) / 32;
set r =
((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024;
set s1 = 2
-root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024));
set t1 = 2
-root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))));
set t2 = 2
-root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))));
thus (((((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (3_root_of_quartic a0,a1,a2,a3)) + (((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((1_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((2_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3)) =
(((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2)))
by A2, A3, A4, A5
.=
(((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) * (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))))) + ((a3 * a3) / 16)) * (- (a3 / 2)))
by Th1
.=
(((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2)))
by Th1
.=
(((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- ((2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) |^ 2)) + ((a3 * a3) / 16)) * (- (a3 / 2)))
by Th8
.=
(((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) - (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2))) + (((- (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))))))) + ((a3 * a3) / 16)) * (- (a3 / 2)))
by Th8
.=
((a2 - ((3 * (a3 |^ 2)) / 8)) + ((a3 * a3) / 8)) * (- (a3 / 2))
.=
((a2 - ((3 * (a3 * a3)) / 8)) + ((a3 * a3) / 8)) * (- (a3 / 2))
by Th1
.=
(((a3 * a3) * a3) / 8) - ((a2 * a3) / 2)
.=
((a3 |^ 3) / 8) - (((4 * a2) * a3) / 8)
by Th2
.=
- a1
by A1
;
:: thesis: verum end; suppose A6:
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0
;
:: thesis: (((((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (3_root_of_quartic a0,a1,a2,a3)) + (((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((1_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((2_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3)) = - a1A7:
ex
p,
q,
r,
s1,
s2,
s3 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root (1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s2 = 2
-root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s3 = - (q / (s1 * s2)) &
1_root_of_quartic a0,
a1,
a2,
a3 = ((s1 + s2) + s3) - (a3 / 4) )
by A6, Def5;
A8:
ex
p,
q,
r,
s1,
s2,
s3 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root (1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s2 = 2
-root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s3 = - (q / (s1 * s2)) &
2_root_of_quartic a0,
a1,
a2,
a3 = (((- s1) - s2) + s3) - (a3 / 4) )
by A6, Def6;
A9:
ex
p,
q,
r,
s1,
s2,
s3 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root (1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s2 = 2
-root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s3 = - (q / (s1 * s2)) &
3_root_of_quartic a0,
a1,
a2,
a3 = (((- s1) + s2) - s3) - (a3 / 4) )
by A6, Def7;
A10:
ex
p,
q,
r,
s1,
s2,
s3 being
complex number st
(
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 &
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 &
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 &
s1 = 2
-root (1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s2 = 2
-root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) &
s3 = - (q / (s1 * s2)) &
4_root_of_quartic a0,
a1,
a2,
a3 = ((s1 - s2) - s3) - (a3 / 4) )
by A6, Def8;
set p =
((8 * a2) - (3 * (a3 |^ 2))) / 32;
set q =
(((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64;
set r =
((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024;
set s1 = 2
-root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)));
set s2 = 2
-root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)));
set s3 =
- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))));
A11:
((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) * ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) <> 0
by A6;
A12:
(2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) =
(2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) |^ 2
by Th1
.=
1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),
(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),
(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))
by Th8
;
A13:
(2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) =
(2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) |^ 2
by Th1
.=
2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),
(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),
(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))
by Th8
;
A14:
(((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (3_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) = - (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2))
by A12, A13, Th19;
then A15:
((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) <> 0
by A11, Th1;
((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) <> 0
by A14, A11, Th1;
then A16:
(2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) <> 0
;
A17:
(- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) =
((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))
by XCMPLX_1:188
.=
((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) * ((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))
by XCMPLX_1:188
.=
((- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) * (- ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64))) / (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))
by XCMPLX_1:77
.=
(((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) * ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64)) / (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))
.=
((3_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) * (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) / (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))
by A14, Th1
.=
3_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),
(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),
(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))
by A15, XCMPLX_1:90
;
thus (((((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (3_root_of_quartic a0,a1,a2,a3)) + (((1_root_of_quartic a0,a1,a2,a3) * (2_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((1_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3))) + (((2_root_of_quartic a0,a1,a2,a3) * (3_root_of_quartic a0,a1,a2,a3)) * (4_root_of_quartic a0,a1,a2,a3)) =
((((((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) + ((2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))) + ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))) * a3) - (((a3 * a3) * a3) / 16)) + (((8 * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))
by A7, A8, A9, A10
.=
(((- (2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) * a3) - (((a3 * a3) * a3) / 16)) + (((8 * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))
by Th18, A12, A13, A17
.=
(((- (((16 * a2) / 32) * a3)) + (((6 * (a3 |^ 2)) / 32) * a3)) - (((a3 * a3) * a3) / 16)) - (((8 * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))
.=
(((- ((a2 / 2) * a3)) + (((6 * (a3 * a3)) / 32) * a3)) - (((a3 * a3) * a3) / 16)) - (((8 * (2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))))))
by Th1
.=
((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))
.=
((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / (((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))) / ((2 -root (1_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) * (2 -root (2_root_of_cubic (- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))))))))
by XCMPLX_1:82
.=
((- ((a2 * a3) / 2)) + ((((2 * a3) * a3) * a3) / 16)) - (8 * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / 1))
by A16, XCMPLX_1:60
.=
((- a1) + ((((2 * a3) * a3) * a3) / 16)) - ((8 * (a3 |^ 3)) / 64)
.=
((- a1) + ((((2 * a3) * a3) * a3) / 16)) - ((8 * ((a3 * a3) * a3)) / 64)
by Th2
.=
- a1
;
:: thesis: verum end;