let z, a0, a1, a2, s1, q, r be Complex; ( 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 that
A1:
q = ((3 * a1) - (a2 |^ 2)) / 9
and
A2:
q = 0
; ( 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) ) ) )
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>);
A3: (((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 Th7
.=
3 * q
by A2
;
set x = z + (a2 / 3);
assume A4:
r = ((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54
; ( 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 A5:
s1 = 3 -root (2 * r)
; ( (((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) ) )
A6:
- (((2 * (s1 / 2)) + ((- (s1 / 2)) + (((s1 / 2) * (2 -root 3)) * <i>))) + ((- (s1 / 2)) - (((s1 / 2) * (2 -root 3)) * <i>))) = 0
;
A7: (s1 * s1) * s1 =
s1 |^ 3
by Th2
.=
2 * r
by A5, Th7
;
- (((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 Th7
.=
- (2 * r)
by A7
;
then A8:
( ((((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, A3, 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, A4, Th13;
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 A8; verum