let a, b, c, d be Real; for z being Complex st a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 holds
for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>)
let z be Complex; ( a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 implies for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) )
assume A1:
a <> 0
; ( not Polynom (a,b,c,d,z) = 0 or not Im z = 0 or for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) )
set p = (((3 * a) * c) - (b ^2)) / (3 * (a ^2));
set b9 = c / a;
A2:
a = a + (0 * <i>)
;
set q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)));
set c9 = d / a;
set a9 = b / a;
set y = Im z;
set x = Re z;
assume that
A3:
Polynom (a,b,c,d,z) = 0
and
A4:
Im z = 0
; for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) holds
z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>)
A5:
z = (Re z) + ((Im z) * <i>)
by COMPLEX1:13;
0 =
(((a * ((Re (z ^3)) + ((Im (z ^3)) * <i>))) + (b * (z ^2))) + (c * z)) + d
by A3, COMPLEX1:13
.=
(((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * <i>))) + (b * (z ^2))) + (c * z)) + d
by Th5
.=
(((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))) + (b * (z ^2))) + (c * z)) + d
by Th5
.=
((((a + (0 * <i>)) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:13
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))) * (Im a))) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:82
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) - (0 * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))) * (Im a))) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A2, COMPLEX1:12
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) - 0) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>))) * 0)) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A2, COMPLEX1:12
.=
((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) - 0) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + 0) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
((((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
(((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * <i>)) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A2, COMPLEX1:12
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) + ((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * <i>)) + (b * ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((c * (Re z)) + ((c * (Im z)) * <i>))) + d
by A2, A5, COMPLEX1:12
;
then 0 =
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * 0))) + (b * (((Re z) ^2) - 0))) + (c * (Re z))) + d) + ((((a * ((- (0 |^ 3)) + 0)) + (b * 0)) + 0) * <i>)
by A4
.=
((((a * ((Re z) |^ 3)) + (b * ((Re z) ^2))) + (c * (Re z))) + d) + (((a * 0) + 0) * <i>)
by NEWTON:11
;
then A6:
Polynom (a,b,c,d,(Re z)) = 0
;
A7:
d / a = d / a
;
((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3 = (1 / 3) * ((((3 * a) * c) - (b ^2)) / (3 * (a ^2)))
;
then A8:
((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3 = (((3 * a) * c) - (b ^2)) / (((a ^2) * 3) * 3)
by XCMPLX_1:103;
A9: - (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2) =
- (((b / (3 * a)) |^ 3) + ((1 / 2) * ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))))
.=
- (((b / (3 * a)) |^ 3) + ((((3 * a) * d) - (b * c)) / (((a ^2) * 3) * 2)))
by XCMPLX_1:103
.=
(- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))
;
let u, v, x1 be Real; ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) implies z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) )
assume that
A10:
( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) )
and
A11:
((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0
; ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) )
( b / a = b / a & c / a = c / a )
;
then
Polynom (1,0,((((3 * a) * c) - (b ^2)) / (3 * (a ^2))),((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))),x1) = 0
by A1, A10, A6, A7, POLYEQ_1:16;
then
( x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) )
by A10, A11, POLYEQ_1:19;
hence
( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * <i>) )
by A4, A10, A8, A9, COMPLEX1:13; verum