set q = ((3 * a1) - (a2 |^ 2)) / 9;
set r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54;
set s = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2));
set s1 = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))));
set s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))));
set IT = ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3);
thus ( (3 * a1) - (a2 |^ 2) = 0 implies ex IT, r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & IT = s1 - (a2 / 3) ) ) :: thesis: ( not (3 * a1) - (a2 |^ 2) = 0 implies ex b₁, q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b₁ = (s1 + s2) - (a2 / 3) ) )

proof

set r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54;
set s1 = 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54));
set IT = (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3);
assume (3 * a1) - (a2 |^ 2) = 0 ; :: thesis: ex IT, r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & IT = s1 - (a2 / 3) )
take (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) ; :: thesis: ex r, s1 being Complex st
( r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) & (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) = s1 - (a2 / 3) )
take ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 ; :: thesis: ex s1 being Complex st
( ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) & (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) = s1 - (a2 / 3) )
take 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) ; :: thesis: ( ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) = 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) & (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) = (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) )
thus ( ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) = 3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54)) & (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) = (3 -root (2 * (((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54))) - (a2 / 3) ) ; :: thesis: verum

end;

assume (3 * a1) - (a2 |^ 2) <> 0 ; :: thesis: ex b₁, q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & b₁ = (s1 + s2) - (a2 / 3) )
take ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) ; :: thesis: ex q, r, s, s1, s2 being Complex st
( q = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root ((q |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - (q / s1) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = (s1 + s2) - (a2 / 3) )
take ((3 * a1) - (a2 |^ 2)) / 9 ; :: thesis: ex r, s, s1, s2 being Complex st
( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + (r |^ 2)) & s1 = 3 -root (r + s) & s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / s1) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = (s1 + s2) - (a2 / 3) )
take ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 ; :: thesis: ex s, s1, s2 being Complex st
( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) & s1 = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + s) & s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / s1) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = (s1 + s2) - (a2 / 3) )
take 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) ; :: thesis: ex s1, s2 being Complex st
( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) & s1 = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) & s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / s1) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = (s1 + s2) - (a2 / 3) )
take 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) ; :: thesis: ex s2 being Complex st
( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) & 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) & s2 = - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + s2) - (a2 / 3) )
take - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) ; :: thesis: ( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) & 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) & - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) = - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) )
thus ( ((3 * a1) - (a2 |^ 2)) / 9 = ((3 * a1) - (a2 |^ 2)) / 9 & ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) = 2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)) & 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) = 3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))) & - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) = - ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))) & ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) = ((3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2))))) + (- ((((3 * a1) - (a2 |^ 2)) / 9) / (3 -root ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) + (2 -root (((((3 * a1) - (a2 |^ 2)) / 9) |^ 3) + ((((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54) |^ 2)))))))) - (a2 / 3) ) ; :: thesis: verum