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) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 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) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 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) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 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) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0 )
assume A3: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a ) ; :: thesis: (((y |^ 3) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0
set q2 = ((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3);
set p2 = ((3 * (h ^2 )) + (2 * (a1 * h))) + a2;
set p0 = (3 * h) + a1;
A4: ((y |^ 3) + ((((3 * h) + a1) * (y ^2 )) + ((((3 * (h ^2 )) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3)) = 0 by A1, A2, A3, Th15;
A5: (3 * h) + a1 = 0

proof

(3 * h) + a1 = (- (3 * (b / (3 * a)))) + a1 by A3
.= (- (3 * (((3 * a) " ) * b))) + a1 by XCMPLX_0:def 9
.= (- (3 * (((3 " ) * (a " )) * b))) + a1 by XCMPLX_1:205
.= (- (((3 * (3 " )) * (a " )) * b)) + a1
.= (- (b / a)) + a1 by XCMPLX_0:def 9 ;
hence (3 * h) + a1 = 0 by A3; :: thesis: verum

end;

A6: 3 * a <> 0 by A1;
A7: ((3 * (h ^2 )) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))

proof

set t = ((3 * a) " ) * b;
A8: (3 * a) / (3 * a) = 1 by A6, XCMPLX_1:60;
((3 * (h ^2 )) + (2 * (a1 * h))) + a2 = ((3 * ((b / (3 * a)) ^2 )) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by A3
.= ((3 * ((((3 * a) " ) * b) ^2 )) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def 9
.= ((((3 * ((3 * a) " )) * b) * (((3 * a) " ) * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2
.= ((((3 * ((3 " ) * (a " ))) * b) * (((3 * a) " ) * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:205
.= (((b / a) * (((3 * a) " ) * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def 9
.= (((b / a) * (b / (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def 9
.= (((b * b) / (a * (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:77
.= (((b ^2 ) / (3 * (a ^2 ))) - (2 * ((b / a) * (b / (3 * a))))) + (c / a) by A3
.= (((b ^2 ) / (3 * (a ^2 ))) - (2 * ((b * b) / (a * (3 * a))))) + (c / a) by XCMPLX_1:77
.= (- ((b ^2 ) / (3 * (a ^2 )))) + (((3 * a) / (3 * a)) * (c / a)) by A8
.= (- ((b ^2 ) / (3 * (a ^2 )))) + (((3 * a) * c) / ((3 * a) * a)) by XCMPLX_1:77
.= (((3 * a) * c) / (3 * (a ^2 ))) - ((b ^2 ) / (3 * (a ^2 )))
.= (((3 * a) * c) * ((3 * (a ^2 )) " )) - ((b ^2 ) / (3 * (a ^2 ))) by XCMPLX_0:def 9
.= (((3 * a) * c) * ((3 * (a ^2 )) " )) - ((b ^2 ) * ((3 * (a ^2 )) " )) by XCMPLX_0:def 9
.= (((3 * a) * c) - (b ^2 )) * ((3 * (a ^2 )) " ) ;
hence ((3 * (h ^2 )) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2 )) / (3 * (a ^2 )) by XCMPLX_0:def 9; :: thesis: verum

end;

((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))

proof

set t = 3 * a;
set a6 = b / (3 * a);
A9: b / a = (3 * b) / (3 * a) by XCMPLX_1:92;
A10: ((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3) = (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + ((- ((c / a) * (b / (3 * a)))) + (d / a)) by A3
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + ((- ((b * c) / ((3 * a) * a))) + (d / a)) by XCMPLX_1:77
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + ((- ((b * c) / (3 * (a ^2 )))) + (1 * (d / a)))
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + ((- ((b * c) / (3 * (a ^2 )))) + (((3 * a) / (3 * a)) * (d / a))) by A6, XCMPLX_1:60
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + (((3 * a) / (3 * a)) * (d / a))) - ((b * c) / (3 * (a ^2 )))
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + (((3 * a) * d) / ((3 * a) * a))) - ((b * c) / (3 * (a ^2 ))) by XCMPLX_1:77
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + (((3 * a) * d) * ((3 * (a ^2 )) " ))) - ((b * c) / (3 * (a ^2 ))) by XCMPLX_0:def 9
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + (((3 * a) * d) * ((3 * (a ^2 )) " ))) - ((b * c) * ((3 * (a ^2 )) " )) by XCMPLX_0:def 9
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2 ))) + ((((3 * a) * d) - (b * c)) * ((3 * (a ^2 )) " ))
.= (((- (b / (3 * a))) |^ (2 + 1)) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_0:def 9
.= ((((- (b / (3 * a))) |^ (1 + 1)) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by NEWTON:11
.= (((((- (b / (3 * a))) |^ 1) * (- (b / (3 * a)))) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by NEWTON:11
.= ((((- (b / (3 * a))) |^ 1) * ((- (b / (3 * a))) ^2 )) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))
.= ((((- (b / (3 * a))) to_power 1) * ((- (b / (3 * a))) ^2 )) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by POWER:46
.= (((- (b / (3 * a))) * ((b / (3 * a)) ^2 )) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by POWER:30
.= (((- (b / (3 * a))) * ((b ^2 ) / ((3 * a) ^2 ))) + ((b / a) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_1:77
.= (((- (b / (3 * a))) * ((b ^2 ) / ((3 * a) ^2 ))) + ((b / a) * ((b ^2 ) / ((3 * a) ^2 )))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_1:77
.= (((b / a) - (b / (3 * a))) * ((b ^2 ) / ((3 * a) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))
.= ((((3 * b) * ((3 * a) " )) - ((1 * b) / (3 * a))) * ((b ^2 ) / ((3 * a) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by A9, XCMPLX_0:def 9
.= ((((3 * b) * ((3 * a) " )) - ((1 * b) * ((3 * a) " ))) * ((b ^2 ) / ((3 * a) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_0:def 9
.= (2 * ((b * ((3 * a) " )) * ((b ^2 ) / ((3 * a) ^2 )))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))
.= (2 * ((b / (3 * a)) * ((b ^2 ) / ((3 * a) ^2 )))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_0:def 9
.= (2 * ((b / (3 * a)) * ((b / (3 * a)) ^2 ))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by XCMPLX_1:77 ;
(b / (3 * a)) |^ 3 = (b / (3 * a)) |^ (2 + 1)
.= ((b / (3 * a)) |^ (1 + 1)) * (b / (3 * a)) by NEWTON:11
.= (((b / (3 * a)) |^ 1) * (b / (3 * a))) * (b / (3 * a)) by NEWTON:11
.= ((b / (3 * a)) |^ 1) * ((b / (3 * a)) ^2 )
.= ((b / (3 * a)) to_power 1) * ((b / (3 * a)) ^2 ) by POWER:46 ;
hence ((h |^ 3) + (a1 * (h ^2 ))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 ))) by A10, POWER:30; :: thesis: verum

end;

hence (((y |^ 3) + (0 * (y ^2 ))) + (((((3 * a) * c) - (b ^2 )) / (3 * (a ^2 ))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2 )))) = 0 by A4, A5, A7; :: thesis: verum