let z, a1, a2, a0, s1, q, r be complex number ; :: thesis: ( q = ((3 * a1) - (a2 |^ 2)) / 9 & q = 0 & r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 & s1 = 3 -root (2 * r) implies ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) ) )
assume A1: ( q = ((3 * a1) - (a2 |^ 2)) / 9 & q = 0 ) ; :: thesis: ( not r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 or not s1 = 3 -root (2 * r) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) ) )
assume A2: r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 ; :: thesis: ( not s1 = 3 -root (2 * r) or ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) ) )
assume A3: s1 = 3 -root (2 * r) ; :: thesis: ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) )
set x = z + (a2 / 3);
z = (z + (a2 / 3)) - (a2 / 3) ;
then A4: ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff (((z + (a2 / 3)) |^ 3) + ((3 * q) * (z + (a2 / 3)))) - (2 * r) = 0 ) by A1, A2, Th14;
A5: (s1 * s1) * s1 = s1 |^ 3 by Th2
.= 2 * r by A3, Th8 ;
set t = s1 / 2;
set x1 = 2 * (s1 / 2);
set x2 = (- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> );
set x3 = (- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> );
A6: - (((2 * (s1 / 2)) + ((- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> ))) + ((- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> ))) = 0 ;
A7: (((2 * (s1 / 2)) * ((- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> ))) + ((2 * (s1 / 2)) * ((- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> )))) + (((- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> )) * ((- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> ))) = (- ((3 * (s1 / 2)) * (s1 / 2))) - ((((s1 / 2) * (s1 / 2)) * ((2 -root 3) * (2 -root 3))) * (- 1))
.= (- ((3 * (s1 / 2)) * (s1 / 2))) - ((((s1 / 2) * (s1 / 2)) * ((2 -root 3) |^ 2)) * (- 1)) by Th1
.= (- ((3 * (s1 / 2)) * (s1 / 2))) - ((((s1 / 2) * (s1 / 2)) * 3) * (- 1)) by Th8
.= 3 * q by A1 ;
- (((2 * (s1 / 2)) * ((- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> ))) * ((- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> ))) = (- (2 * (s1 / 2))) * (((s1 / 2) * (s1 / 2)) - ((((s1 / 2) * (s1 / 2)) * ((2 -root 3) * (2 -root 3))) * (- 1)))
.= (- (2 * (s1 / 2))) * (((s1 / 2) * (s1 / 2)) - ((((s1 / 2) * (s1 / 2)) * ((2 -root 3) |^ 2)) * (- 1))) by Th1
.= (- (2 * (s1 / 2))) * (((s1 / 2) * (s1 / 2)) - ((((s1 / 2) * (s1 / 2)) * 3) * (- 1))) by Th8
.= - (2 * r) by A5 ;
then ( ((((z + (a2 / 3)) |^ 3) + (0 * ((z + (a2 / 3)) |^ 2))) + ((3 * q) * (z + (a2 / 3)))) + (- (2 * r)) = 0 iff ( z + (a2 / 3) = 2 * (s1 / 2) or z + (a2 / 3) = (- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i> ) or z + (a2 / 3) = (- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i> ) ) ) by A6, A7, Th15;
hence ( (((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 - (a2 / 3) or z = ((- (s1 / 2)) - (a2 / 3)) + (((s1 * (2 -root 3)) * <i> ) / 2) or z = ((- (s1 / 2)) - (a2 / 3)) - (((s1 * (2 -root 3)) * <i> ) / 2) ) ) by A4; :: thesis: verum