let a, c, d be Real; :: thesis:
let z be Element of 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:29
.= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + ((Im (z ^3 )) * ))) + (c * z)) + d by Th11
.= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * ))) + (c * z)) + d by Th11
.= (((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:29
.= (((((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:def 10
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= (((((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:28
.= ((((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:28
.= ((((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:28
.= ((((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:28
.= ((((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:28
.= (((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:12, COMPLEX1:28;
then (a * ((- (((Im z) |^ 2) * (Im z))) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z)) = 0 by NEWTON:11;
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:90;
then ((Im z) |^ 1) * (Im z) = ((a * (3 * ((Re z) ^2 ))) + c) / a by NEWTON:11;
then A6: (Im z) ^2 = ((((3 * ((Re z) ^2 )) * a) / a) + (c / a)) + (0 / a) by NEWTON:10;
then A7: ( z = (Re z) + ((Im z) * ) & (Im z) ^2 = ((3 * ((Re z) ^2 )) + (c / a)) + (0 * (a " )) ) by A1, COMPLEX1:29, XCMPLX_1:90;
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:104
.= 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:104;
((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z)))) + (c * (Im z))) + 0 = 0 by A5, COMPLEX1:12, COMPLEX1:28;
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:90;
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 by NEWTON:10
.= (((a * ((Re z) |^ 3)) - (a * ((9 * (((Re z) |^ (1 + 1)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d by NEWTON:11
.= (((a * ((Re z) |^ 3)) - (a * (((9 * ((Re z) |^ (2 + 1))) + ((3 * (Re z)) * (c / a))) + 0 ))) + (c * (Re z))) + d by NEWTON:11
.= (((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:89
.= (((- (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:89;
then 0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2 ))) + ((((2 / 8) * c) / a) * (Re z))) + ((- d) / (8 * a)) by XCMPLX_1:84;
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:104;
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

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, Th20; :: 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, Th20; :: 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, Th20; :: 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: