let z, a0, a1, a2, s1, s2, q, r, s be Complex; :: thesis: ( q = ((3 * a1) - (a2 |^ 2)) / 9 & q <> 0 & 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) implies ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) )
assume that
A1: q = ((3 * a1) - (a2 |^ 2)) / 9 and
A2: q <> 0 ; :: thesis: ( not r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 or not s = 2 -root ((q |^ 3) + (r |^ 2)) or not s1 = 3 -root (r + s) or not s2 = - (q / s1) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) )
assume A3: r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 ; :: thesis: ( not s = 2 -root ((q |^ 3) + (r |^ 2)) or not s1 = 3 -root (r + s) or not s2 = - (q / s1) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) )
set t = (s1 + s2) / 2;
set d = (s1 - s2) / 2;
set x = z + (a2 / 3);
set x1 = 2 * ((s1 + s2) / 2);
set x2 = (- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>);
set x3 = (- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>);
A4: - (((2 * ((s1 + s2) / 2)) + ((- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) + ((- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) = 0 ;
assume A5: s = 2 -root ((q |^ 3) + (r |^ 2)) ; :: thesis: ( not s1 = 3 -root (r + s) or not s2 = - (q / s1) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) )
assume A6: s1 = 3 -root (r + s) ; :: thesis: ( not s2 = - (q / s1) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) )
A7: s1 <> 0

proof

assume s1 = 0 ; :: thesis: contradiction
then A8: 0 = s1 |^ 3 by NEWTON:11
.= r + s by A6, Th7 ;
(q |^ 3) + (r |^ 2) = s |^ 2 by A5, Th7
.= s * s by Th1
.= (- s) * (- s)
.= r |^ 2 by A8, Th1 ;
then (q * q) * q = 0 by Th2;
hence contradiction by A2; :: thesis: verum

end;

assume A9: s2 = - (q / s1) ; :: thesis: ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) )
then A10: (s2 * s2) * s2 = - (((q / s1) * (q / s1)) * (q / s1))
.= - (((q * q) / (s1 * s1)) * (q / s1)) by XCMPLX_1:76
.= - (((q * q) * q) / ((s1 * s1) * s1)) by XCMPLX_1:76
.= - (((q * q) * q) / ((3 -root (r + s)) |^ 3)) by A6, Th2
.= - (((q * q) * q) / (r + s)) by Th7
.= - ((q |^ 3) / (r + s)) by Th2 ;
A11: (s1 * s1) * s1 = s1 |^ 3 by Th2
.= r + s by A6, Th7 ;
A12: (((2 * ((s1 + s2) / 2)) * ((- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) + ((2 * ((s1 + s2) / 2)) * ((- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>)))) + (((- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>)) * ((- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) = (- ((3 * ((s1 + s2) / 2)) * ((s1 + s2) / 2))) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * ((2 -root 3) * (2 -root 3))) * (- 1))
.= (- ((3 * ((s1 + s2) / 2)) * ((s1 + s2) / 2))) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * ((2 -root 3) |^ 2)) * (- 1)) by Th1
.= (- ((3 * ((s1 + s2) / 2)) * ((s1 + s2) / 2))) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * 3) * (- 1)) by Th7
.= 3 * (s1 * (q / s1)) by A9
.= 3 * ((s1 * q) / s1) by XCMPLX_1:74
.= 3 * q by A7, XCMPLX_1:89 ;
- (((2 * ((s1 + s2) / 2)) * ((- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) * ((- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>))) = (- (2 * ((s1 + s2) / 2))) * ((((s1 + s2) / 2) * ((s1 + s2) / 2)) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * ((2 -root 3) * (2 -root 3))) * (- 1)))
.= (- (2 * ((s1 + s2) / 2))) * ((((s1 + s2) / 2) * ((s1 + s2) / 2)) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * ((2 -root 3) |^ 2)) * (- 1))) by Th1
.= (- (2 * ((s1 + s2) / 2))) * ((((s1 + s2) / 2) * ((s1 + s2) / 2)) - (((((s1 - s2) / 2) * ((s1 - s2) / 2)) * 3) * (- 1))) by Th7
.= - ((r + s) - ((q |^ 3) / (r + s))) by A11, A10
.= - ((((r + s) * (r + s)) / (r + s)) - ((q |^ 3) / (r + s))) by A11, A7, XCMPLX_1:89
.= - (((((r * r) + ((2 * s) * r)) + (s * s)) - (q |^ 3)) / (r + s)) by XCMPLX_1:120
.= - (((((r * r) + ((2 * s) * r)) + ((2 -root ((q |^ 3) + (r |^ 2))) |^ 2)) - (q |^ 3)) / (r + s)) by A5, Th1
.= - (((((r * r) + ((2 * s) * r)) + ((q |^ 3) + (r |^ 2))) - (q |^ 3)) / (r + s)) by Th7
.= - ((((r * r) + ((2 * s) * r)) + (r |^ 2)) / (r + s))
.= - ((((r * r) + ((2 * s) * r)) + (r * r)) / (r + s)) by Th1
.= - (((2 * r) * (r + s)) / (r + s))
.= - (2 * r) by A11, A7, XCMPLX_1:89 ;
then A13: ( ((((z + (a2 / 3)) |^ 3) + (0 * ((z + (a2 / 3)) |^ 2))) + ((3 * q) * (z + (a2 / 3)))) + (- (2 * r)) = 0 iff ( z + (a2 / 3) = 2 * ((s1 + s2) / 2) or z + (a2 / 3) = (- ((s1 + s2) / 2)) + ((((s1 - s2) / 2) * (2 -root 3)) * <i>) or z + (a2 / 3) = (- ((s1 + s2) / 2)) - ((((s1 - s2) / 2) * (2 -root 3)) * <i>) ) ) by A4, A12, Th14;
z = (z + (a2 / 3)) - (a2 / 3) ;
then ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((z + (a2 / 3)) |^ 3) + ((3 * q) * (z + (a2 / 3)))) - (2 * r) = 0 ) by A1, A3, Th13;
hence ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = (s1 + s2) - (a2 / 3) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) + ((((s1 - s2) * (2 -root 3)) * <i>) / 2) or z = ((- ((s1 + s2) / 2)) - (a2 / 3)) - ((((s1 - s2) * (2 -root 3)) * <i>) / 2) ) ) by A13; :: thesis: verum