let a0, a1, a2, a3 be Complex; (((1_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)) = a0
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
;
(((1_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)) = a0set 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))))));
A2:
( ex
p,
r,
s1 being
Complex 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) ) & ex
p,
r,
s1 being
Complex 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, Def7, Def8;
( ex
p,
r,
s1 being
Complex 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) ) & ex
p,
r,
s1 being
Complex 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, Def5, Def6;
hence (((1_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)) * ((- ((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))
by A2
.=
((- ((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)) * ((- ((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))
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)) * ((- ((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))
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)) * ((- ((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))
by Th7
.=
((- (- (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)) * ((- (- (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))
by Th7
.=
((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) + (((((2 * 2) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 16)) + (((((a3 * a3) * a3) * a3) / 16) / 16)) - (4 * ((2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))) * (2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)))))
.=
((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) + ((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 16)) + (((((a3 * a3) * a3) * a3) / 16) / 16)) - (4 * ((2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))) |^ 2))
by Th1
.=
(((4 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) + ((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 16)) + (((((a3 * a3) * a3) * a3) / 16) / 16)) - (4 * (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)))
by Th7
.=
(((4 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2)) + ((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 16)) + (((((a3 * a3) * a3) * a3) / 16) / 16)) - (4 * (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)))
by Th1
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + ((((a3 * a3) * (a3 * a3)) / 16) / 16)) + (4 * (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + ((((a3 * a3) * (a3 |^ 2)) / 16) / 16)) + (4 * (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))
by Th1
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + (((a3 * a3) * (a3 |^ 2)) / 256)) + (((a0 - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)) - ((3 * (a3 |^ 4)) / 256))
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + (((a3 * a3) * (a3 |^ 2)) / 256)) + (((a0 - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)) - ((3 * (((a3 * a3) * a3) * a3)) / 256))
by Th3
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + (((a3 * a3) * (a3 |^ 2)) / 256)) + (((a0 - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)) - ((((3 * a3) * a3) * (a3 * a3)) / 256))
.=
(((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4) + (((a3 * a3) * (a3 |^ 2)) / 256)) + (((a0 - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)) - ((((3 * a3) * a3) * (a3 |^ 2)) / 256))
by Th1
.=
(((a0 + ((a2 * (a3 * a3)) / 16)) - ((((4 * (a3 |^ 2)) * a3) * a3) / 128)) - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)
.=
(((a0 + ((a2 * (a3 |^ 2)) / 16)) - ((((a3 |^ 2) * a3) * a3) / 32)) - ((a3 * a1) / 4)) + (((a3 |^ 2) * a2) / 16)
by Th1
.=
((a0 + (((2 * a2) * (a3 |^ 2)) / 16)) - ((((a3 |^ 2) * a3) * a3) / 32)) - ((a3 * a1) / 4)
.=
((a0 + (((2 * a2) * (a3 * a3)) / 16)) - ((((a3 |^ 2) * a3) * a3) / 32)) - ((a3 * a1) / 4)
by Th1
.=
((a0 + ((((4 * a2) * a3) * a3) / 32)) - ((((a3 * a3) * a3) * a3) / 32)) - (((8 * a3) * a1) / 32)
by Th1
.=
a0 + ((((((4 * a2) * a3) - ((a3 * a3) * a3)) - (8 * a1)) * a3) / 32)
.=
a0 + ((((((4 * a2) * a3) - (a3 |^ 3)) - (8 * a1)) * a3) / 32)
by Th2
.=
a0
by A1
;
verum end; suppose A3:
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0
;
(((1_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)) = a0then A4:
( ex
p,
q,
r,
s1,
s2,
s3 being
Complex 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) ) & ex
p,
q,
r,
s1,
s2,
s3 being
Complex 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 Def7, 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)))))));
A5:
(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 Th7
;
set r1 =
(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)))));
set r2 =
(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)))));
set r3 =
(- (((((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))))))));
A6:
(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 Th7
;
then A7:
(((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 A5, Th19;
A8:
((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) * ((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) <> 0
by A3;
then
((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 A7, Th1;
then A9:
(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
;
A10:
((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 A8, A7, Th1;
A11:
(- (((((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:187
.=
((- ((((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:187
.=
((- ((((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:76
.=
(((((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 A7, 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 A10, XCMPLX_1:89
;
then 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 (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))))))))) = - (2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))
by A6, A5, Th17;
( ex
p,
q,
r,
s1,
s2,
s3 being
Complex 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) ) & ex
p,
q,
r,
s1,
s2,
s3 being
Complex 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 A3, Def5, Def6;
hence (((1_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)))))))))) * ((((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))))))))))) - (4 * (((((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)))))) * ((- (((((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))))))))))) + (((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))))))))))))) - (((((((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) / 8)) - ((((2 * (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) * a3) / 16) / 16)
by A4
.=
(((((- (2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32))) * (- (2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) - (4 * (((((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) / 8)) - ((((2 * (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) * a3) / 16) / 16)
by A6, A5, A11, A12, Th18
.=
(((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) - (4 * (((((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) / 8)) - ((((2 * (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) * a3) / 16) / 16)
.=
(((((4 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) - (4 * (((((8 * a2) - (3 * (a3 |^ 2))) / 32) * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)))) + ((((2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 8)) - ((((2 * (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) * a3) / 16) / 16)
by Th1
.=
(((4 * (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)) + ((((2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 8)) + ((2 * 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 (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) / 16)
.=
(((4 * (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)) + ((((2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 8)) + ((2 * a3) * (((((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)))))))))) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by XCMPLX_1:81
.=
(((4 * (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024)) + ((((2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)) * a3) * a3) / 8)) + ((2 * a3) * (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / 1))) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by A9, XCMPLX_1:60
.=
((((4 * ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4)))) / 1024) + ((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4)) + (((2 * a3) * (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3))) / 64)) + (((((a3 * a3) * a3) * a3) / 16) / 16)
.=
((((4 * ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 * a3)) * a2)) - (3 * (a3 |^ 4)))) / 1024) + ((((((8 * a2) - (3 * (a3 |^ 2))) / 32) * a3) * a3) / 4)) + (((2 * a3) * (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3))) / 64)) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by Th1
.=
((((4 * ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 * a3)) * a2)) - (3 * (a3 |^ 4)))) / 1024) + ((((((8 * a2) - (3 * (a3 * a3))) / 32) * a3) * a3) / 4)) + (((2 * a3) * (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3))) / 64)) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by Th1
.=
((((4 * ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 * a3)) * a2)) - (3 * (((a3 * a3) * a3) * a3)))) / 1024) + ((((((8 * a2) - (3 * (a3 * a3))) / 32) * a3) * a3) / 4)) + (((2 * a3) * (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3))) / 64)) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by Th3
.=
((((4 * ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 * a3)) * a2)) - (3 * (((a3 * a3) * a3) * a3)))) / 1024) + ((((((8 * a2) - (3 * (a3 * a3))) / 32) * a3) * a3) / 4)) + (((2 * a3) * (((8 * a1) - ((4 * a2) * a3)) + ((a3 * a3) * a3))) / 64)) + (((((a3 * a3) * a3) * a3) / 16) / 16)
by Th2
.=
a0
;
verum end;