let a, b, c, d, x be Real; :: thesis: ( a <> 0 & Polynom (a,b,c,d,x) = 0 implies for a1, a2, a3, h, y being Real st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume A1: a <> 0 ; :: thesis: ( not Polynom (a,b,c,d,x) = 0 or for a1, a2, a3, h, y being Real st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume A2: Polynom (a,b,c,d,x) = 0 ; :: thesis: for a1, a2, a3, h, y being Real st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0
let a1, a2, a3, h, y be Real; :: thesis: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a implies ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume that
A3: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) ) and
A4: ( a1 = b / a & a2 = c / a & a3 = d / a ) ; :: thesis: ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0
0 = (a ") * (((a * (x |^ 3)) + (b * (x ^2))) + ((c * x) + d)) by A2
.= ((((a ") * a) * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d))
.= ((1 * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d)) by A1, XCMPLX_0:def 7
.= (((x |^ 3) + (((a ") * b) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d)
.= (((x |^ 3) + ((b / a) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d) by XCMPLX_0:def 9
.= (((x |^ 3) + ((b / a) * (x ^2))) + ((c / a) * x)) + ((a ") * d) by XCMPLX_0:def 9
.= (((x |^ 3) + (a1 * (x ^2))) + (a2 * x)) + a3 by A4, XCMPLX_0:def 9 ;
then 0 = (((((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)) + (((a1 * (y ^2)) + ((2 * (a1 * h)) * y)) + (a1 * (h ^2)))) + (a2 * (y + h))) + a3 by A3, Th14
.= (((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (((2 * (a1 * h)) * y) + (a1 * (y ^2)))) + ((a2 * y) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3))) ;
hence ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ; :: thesis: verum