let a, c, d be Real; for z being Complex st a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 holds
for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>)
let z be Complex; ( a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 implies for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) )
assume A1:
a <> 0
; ( not Im z <> 0 or not Polynom (a,0,c,d,z) = 0 or for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) )
set y = Im z;
set x = Re z;
assume that
A2:
Im z <> 0
and
A3:
Polynom (a,0,c,d,z) = 0
; for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) holds
z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>)
A4:
a = a + (0 * <i>)
;
A5: 0 =
(((a * ((Re (z ^3)) + ((Im (z ^3)) * <i>))) + (0 * (z ^2))) + (c * z)) + d
by A3, COMPLEX1:13
.=
((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * <i>))) + (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>))) + (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>))) + (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>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:82
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((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>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((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>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * <i>)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
(((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by COMPLEX1:12
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A4, COMPLEX1:12
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - (0 * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A4, COMPLEX1:12
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A4, COMPLEX1:12
.=
((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * 0)) * <i>)) + (c * ((Re z) + ((Im z) * <i>)))) + d
by A4, COMPLEX1:12
.=
(((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) + (c * (Re z))) + d) + ((((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z))) + 0) * <i>)
;
then
(a * ((- ((Im z) |^ (2 + 1))) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z)) = 0
by COMPLEX1:4, COMPLEX1:12;
then
(a * ((- (((Im z) |^ 2) * (Im z))) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z)) = 0
by NEWTON:6;
then
(((a * ((- ((Im z) |^ 2)) + (3 * ((Re z) ^2)))) + c) + 0) * (Im z) = 0
;
then
(a * ((Im z) |^ 2)) + ((- (a * ((Im z) |^ 2))) + ((a * (3 * ((Re z) ^2))) + c)) = (a * ((Im z) |^ 2)) + 0
by A2, XCMPLX_1:6;
then
(Im z) |^ (1 + 1) = ((a * (3 * ((Re z) ^2))) + c) / a
by A1, XCMPLX_1:89;
then
((Im z) |^ 1) * (Im z) = ((a * (3 * ((Re z) ^2))) + c) / a
by NEWTON:6;
then A6:
(Im z) ^2 = ((((3 * ((Re z) ^2)) * a) / a) + (c / a)) + (0 / a)
;
then A7:
( z = (Re z) + ((Im z) * <i>) & (Im z) ^2 = ((3 * ((Re z) ^2)) + (c / a)) + (0 * (a ")) )
by A1, COMPLEX1:13, XCMPLX_1:89;
set q = - (d / (8 * a));
set pp = c / (4 * a);
let u, v be Real; ( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) implies z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) )
set m = 3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))));
set n = 3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))));
A8: (c / (4 * a)) / 3 =
(1 / 3) * (c / (4 * a))
.=
c / ((a * 4) * 3)
by XCMPLX_1:103
.=
c / (a * (4 * 3))
;
- ((- (d / (8 * a))) / 2) = (1 / 2) * (d / (8 * a))
;
then A9:
- ((- (d / (8 * a))) / 2) = d / ((a * 8) * 2)
by XCMPLX_1:103;
((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z))) + 0 = 0
by A5, COMPLEX1:4, COMPLEX1:12;
then
((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((3 * ((Re z) ^2)) + (c / a)))) + 0)) + (c * (Re z))) + d = 0
by A1, A5, A6, XCMPLX_1:89;
then 0 =
(((a * ((Re z) |^ 3)) - (a * ((9 * ((Re z) * ((Re z) ^2))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
.=
(((a * ((Re z) |^ 3)) - (a * ((9 * ((((Re z) |^ 1) * (Re z)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
.=
(((a * ((Re z) |^ 3)) - (a * ((9 * (((Re z) |^ (1 + 1)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d
by NEWTON:6
.=
(((a * ((Re z) |^ 3)) - (a * (((9 * ((Re z) |^ (2 + 1))) + ((3 * (Re z)) * (c / a))) + 0))) + (c * (Re z))) + d
by NEWTON:6
.=
(((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * (c * (a / a))))) + (c * (Re z))) + d
.=
(((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * c))) + (c * (Re z))) + d
by A1, XCMPLX_1:88
.=
(((- (8 * a)) * ((Re z) |^ 3)) + ((- (2 * c)) * (Re z))) + d
;
then
(- 1) * 0 = (((8 * a) * ((Re z) |^ 3)) + ((2 * c) * (Re z))) + (- d)
;
then
0 = ((((Re z) |^ 3) * ((8 * a) / (8 * a))) + (((8 * a) ") * ((2 * c) * (Re z)))) + (((8 * a) ") * (- d))
;
then
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + (((2 * c) / (8 * a)) * (Re z))) + (((8 * a) ") * (- d))
by A1, XCMPLX_1:88;
then
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + ((((2 / 8) * c) / a) * (Re z))) + ((- d) / (8 * a))
by XCMPLX_1:83;
then
0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + (((1 / a) * (c / 4)) * (Re z))) + ((- d) / (8 * a))
;
then A10:
Polynom (1,0,(c / (4 * a)),(- (d / (8 * a))),(Re z)) = 0
by XCMPLX_1:103;
assume
( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 )
; ( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) )
then A11:
( Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) )
by A10, POLYEQ_1:19;
((- (d / (8 * a))) ^2) / 4 = ((1 / 2) * (d / (8 * a))) ^2
;
hence
( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * <i>) )
by A9, A12, A8; verum