let a, c, d be Real; :: thesis: for z being Element of 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 / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) holds
z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3)))))
let z be Element of COMPLEX ; :: thesis: ( 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 / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) holds
z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) )
assume A1: a <> 0 ; :: thesis: ( 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 / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) holds
z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) )
assume A2: ( Im z = 0 & Polynom a,0 ,c,d,z = 0 ) ; :: thesis: for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) holds
z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3)))))
let u, v be Real; :: thesis: ( Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) implies z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) )
assume A3: ( Re z = u + v & ((3 * v) * u) + (c / a) = 0 ) ; :: thesis: ( z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) )
set x = Re z;
set y = Im z;
A5: a = a + (0 * <i> ) ;
A7: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29
.= Re z by A2 ;
0 = (((a * ((Re (z ^3 )) + ((Im (z ^3 )) * <i> ))) + (0 * (z ^2 ))) + (c * z)) + d by A2, COMPLEX1:29
.= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + ((Im (z ^3 )) * <i> ))) + (0 * (z ^2 ))) + (c * z)) + d by Th11
.= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2 )) * (Im z))) * <i> ))) + (c * z)) + d by Th11
.= (((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:29
.= (((((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: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))) * <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: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))) * <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: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))) * <i> )))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2 ))) * (Im a))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + 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))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + 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))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d by A5, 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))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d by A5, 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))) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d by A5, 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 )) * <i> )) + (c * ((Re z) + ((Im z) * <i> )))) + d by A5, COMPLEX1:28
.= (((a * (((Re z) |^ 3) - 0 )) + (c * (Re z))) + d) + ((a * (- 0 )) * <i> ) by NEWTON:16, A2
.= ((a * ((Re z) |^ 3)) + (c * (Re z))) + d ;
then (a " ) * (((a * ((Re z) |^ 3)) + (c * (Re z))) + d) = (a " ) * 0 ;
then ((((Re z) |^ 3) * (a / a)) + (((a " ) * c) * (Re z))) + ((a " ) * d) = 0 ;
then A8: Polynom 1,0 ,(c / a),(d / a),(Re z) = 0 by A1, XCMPLX_1:89;
A9: - ((d / a) / 2) = - ((1 / 2) * (d / a))
.= - (d / (a * 2)) by XCMPLX_1:104 ;
A10: ((d / a) ^2 ) / 4 = (1 / 4) * ((d ^2 ) / (a ^2 )) by XCMPLX_1:77
.= (d ^2 ) / ((a ^2 ) * 4) by XCMPLX_1:104 ;
(c / a) / 3 = (1 / 3) * (c / a)
.= c / (a * 3) by XCMPLX_1:104 ;
hence ( z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2 ) / (4 * (a ^2 ))) + ((c / (3 * a)) |^ 3))))) ) by A3, A7, A8, A9, A10, POLYEQ_1:19; :: thesis: verum