let z, a0, a1, a2, s1, s2, q, r, s be Complex; ( 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
; ( 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
; ( 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))
; ( 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)
; ( 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
assume A9:
s2 = - (q / s1)
; ( (((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; verum