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)))))));
set IT = (((- (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 / 4);
thus
( ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex IT, 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) & IT = (2 -root (- (2 * (p + s1)))) - (a3 / 4) ) )
( not ((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0 implies ex b1, 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)) & b1 = (((- s1) + s2) - s3) - (a3 / 4) ) )proof
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 IT =
(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 / 4);
assume
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) = 0
;
ex IT, 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) & IT = (2 -root (- (2 * (p + s1)))) - (a3 / 4) )
take
(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 / 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 (- (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 / 4) = (2 -root (- (2 * (p + s1)))) - (a3 / 4) )
take
((8 * a2) - (3 * (a3 |^ 2))) / 32
;
ex r, s1 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - r) & (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 / 4) = (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + s1)))) - (a3 / 4) )
take
((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024
;
ex s1 being Complex st
( ((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 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 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 / 4) = (2 -root (- (2 * ((((8 * a2) - (3 * (a3 |^ 2))) / 32) + s1)))) - (a3 / 4) )
take
2
-root (((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - (((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024))
;
( ((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 = ((((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)) = 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 / 4) = (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 / 4) )
thus
(
((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
= ((((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)) = 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 / 4) = (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 / 4) )
;
verum
end;
assume
((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3) <> 0
; ex b1, 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)) & b1 = (((- s1) + s2) - s3) - (a3 / 4) )
take
(((- (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 / 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 (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 / 4) = (((- s1) + s2) - s3) - (a3 / 4) )
take
((8 * a2) - (3 * (a3 |^ 2))) / 32
; ex q, r, s1, s2, s3 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((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)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - r),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - r),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) & s3 = - (q / (s1 * s2)) & (((- (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 / 4) = (((- s1) + s2) - s3) - (a3 / 4) )
take
(((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64
; ex r, s1, s2, s3 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((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 ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - r),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) & s2 = 2 -root (2_root_of_cubic ((- (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) |^ 2)),(((((8 * a2) - (3 * (a3 |^ 2))) / 32) |^ 2) - r),(2 * (((8 * a2) - (3 * (a3 |^ 2))) / 32)))) & s3 = - (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / (s1 * s2)) & (((- (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 / 4) = (((- s1) + s2) - s3) - (a3 / 4) )
take
((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024
; ex s1, s2, s3 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & 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)))) & 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)))) & s3 = - (((((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64) / (s1 * s2)) & (((- (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 / 4) = (((- s1) + s2) - s3) - (a3 / 4) )
take
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))))
; ex s2, s3 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & 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)))) & 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)))) & 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))))) * s2)) & (((- (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 / 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)))))) + s2) - s3) - (a3 / 4) )
take
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))))
; ex s3 being Complex st
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & 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)))) & 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))))))) & (((- (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 / 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 (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)))))) - s3) - (a3 / 4) )
take
- (((((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 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & 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 (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 / 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 (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 / 4) )
thus
( ((8 * a2) - (3 * (a3 |^ 2))) / 32 = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & 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 (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 / 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 (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 / 4) )
; verum