let a, b, c, d, x be real number ; :: thesis: ( a <> 0 & Polynom a,b,c,d,x = 0 implies for a1, a2, a3, h, y being real number 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 number 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 number 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 number ; :: 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 A3: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & 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 A3, 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