let a, p, c, q, d, x be real number ; :: thesis: ( a <> 0 & p = c / a & q = d / a & Polynom a,0 ,c,d,x = 0 implies for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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
x = (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 & p = c / a & q = d / a ) ; :: thesis: ( not Polynom a,0 ,c,d,x = 0 or for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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
x = (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: Polynom a,0 ,c,d,x = 0 ; :: thesis: for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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
x = (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 number ; :: thesis: ( x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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: ( x = u + v & ((3 * v) * u) + p = 0 ) ; :: thesis: ( x = (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 x = (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 x = (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))))) )
(a " ) * (((a * (x |^ 3)) + (c * x)) + d) = 0 by A2;
then (((a " ) * a) * (x |^ 3)) + ((a " ) * ((c * x) + d)) = 0 ;
then (1 * (x |^ 3)) + ((a " ) * ((c * x) + d)) = 0 by A1, XCMPLX_0:def 7;
then (x |^ 3) + ((((a " ) * c) * x) + ((a " ) * d)) = 0 ;
then (x |^ 3) + (((c / a) * x) + ((a " ) * d)) = 0 by XCMPLX_0:def 9;
then (x |^ 3) + (((c / a) * x) + (d / a)) = 0 by XCMPLX_0:def 9;
then A4: Polynom 1,0 ,p,q,x = 0 by A1;
A5: p / 3 = c / (3 * a) by A1, XCMPLX_1:79;
A6: - (q / 2) = - (d / (2 * a)) by A1, XCMPLX_1:79;
(q ^2 ) / 4 = ((d ^2 ) / (a ^2 )) / 4 by A1, XCMPLX_1:77;
then (q ^2 ) / 4 = (d ^2 ) / (4 * (a ^2 )) by XCMPLX_1:79;
hence ( x = (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 x = (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 x = (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, A4, A5, A6, Th19; :: thesis: verum