let a, c, d, p, q, x be Real; ( a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 implies for u, v being Real 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 that
A1:
a <> 0
and
A2:
p = c / a
and
A3:
q = d / a
; ( not Polynom (a,0,c,d,x) = 0 or for u, v being Real 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))))) )
A4:
( p / 3 = c / (3 * a) & - (q / 2) = - (d / (2 * a)) )
by A2, A3, XCMPLX_1:78;
assume
Polynom (a,0,c,d,x) = 0
; for u, v being Real 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)))))
then
(a ") * (((a * (x |^ 3)) + (c * x)) + d) = 0
;
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 A5:
Polynom (1,0,p,q,x) = 0
by A2, A3;
(q ^2) / 4 = ((d ^2) / (a ^2)) / 4
by A3, XCMPLX_1:76;
then A6:
(q ^2) / 4 = (d ^2) / (4 * (a ^2))
by XCMPLX_1:78;
let u, v be Real; ( 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
( x = u + v & ((3 * v) * u) + p = 0 )
; ( 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))))) )
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 A5, A4, A6, Th19; verum