let a, c, d be Real; :: thesis:
let z be Complex; :: thesis:
assume A1: a <> 0 ; :: thesis:
set y = Im z;
set x = Re z;
assume that
A2: Im z <> 0 and
A3: Polynom (a,0,c,d,z) = 0 ; :: thesis:
A4: a = a + (0 * ) ;
A5: 0 = (((a * ((Re (z ^3)) + ((Im (z ^3)) * ))) + (0 * (z ^2))) + (c * z)) + d by A3, COMPLEX1:13
.= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * ))) + (c * z)) + d by Th5
.= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * z)) + d by Th5
.= (((a + (0 * )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * ((Re z) + ((Im z) * )))) + 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))) * )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((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))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )) + (c * ((Re z) + ((Im z) * )))) + 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))) * )) + (c * ((Re z) + ((Im z) * )))) + 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)) * )) + (c * ((Re z) + ((Im z) * )))) + 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) * ) ;
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) * ) & (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; :: thesis:
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 ) ; :: thesis:
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;

A12: now :: thesis:

per cases by A11;

case 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))))) ; :: thesis:

hence ( 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)))))) + ((sqrt ((3 * (((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)))))) ^2)) + (c / a))) * ) or 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)))))) + ((- (sqrt ((3 * (((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)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; :: thesis:

end;

case Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ; :: thesis:

hence ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; :: thesis:

end;

case Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ; :: thesis:

hence ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; :: thesis:

end;

((- (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))) * ) 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))) * ) 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))) * ) 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))) * ) 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))) * ) 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))) * ) ) by A9, A12, A8; :: thesis: