let a, c, d be Real; :: thesis: 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 / 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 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))))) )
set y = Im z;
set x = Re z;
assume that
A2: Im z = 0 and
A3: 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)))))
A4: a = a + (0 * <i>) ;
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>))) + (0 * (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>))) + (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) - 0)) + (c * (Re z))) + d) + ((a * (- 0)) * <i>) by A2, NEWTON:11
.= ((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 A5: Polynom (1,0,(c / a),(d / a),(Re z)) = 0 by A1, XCMPLX_1:88;
A6: ((d / a) ^2) / 4 = (1 / 4) * ((d ^2) / (a ^2)) by XCMPLX_1:76
.= (d ^2) / ((a ^2) * 4) by XCMPLX_1:103 ;
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 A7: ( 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))))) )
A8: - ((d / a) / 2) = - ((1 / 2) * (d / a))
.= - (d / (a * 2)) by XCMPLX_1:103 ;
A9: (c / a) / 3 = (1 / 3) * (c / a)
.= c / (a * 3) by XCMPLX_1:103 ;
z = (Re z) + ((Im z) * <i>) by COMPLEX1:13
.= Re z by A2 ;
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 A7, A5, A8, A6, A9, POLYEQ_1:19; :: thesis: verum