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) + (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 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 )
then A2: 3 * a <> 0 ;
assume A3: 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) + (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; :: 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 that
A4: y = x + (b / (3 * a)) and
A5: h = - (b / (3 * a)) and
A6: a1 = b / a and
A7: a2 = c / a and
A8: 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 p0 = (3 * h) + a1;
A9: (3 * h) + a1 = (- (3 * (b / (3 * a)))) + a1 by A5
.= (- (3 * (((3 * a) ") * b))) + a1 by XCMPLX_0:def 9
.= (- (3 * (((3 ") * (a ")) * b))) + a1 by XCMPLX_1:204
.= (- (((3 * (3 ")) * (a ")) * b)) + a1
.= (- (b / a)) + a1 by XCMPLX_0:def 9 ;
set q2 = ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3);
A10: ((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);
A11: b / a = (3 * b) / (3 * a) by XCMPLX_1:91;
A12: (b / (3 * a)) |^ 3 = (b / (3 * a)) |^ (2 + 1)
.= ((b / (3 * a)) |^ (1 + 1)) * (b / (3 * a)) by NEWTON:6
.= (((b / (3 * a)) |^ 1) * (b / (3 * a))) * (b / (3 * a)) by NEWTON:6
.= ((b / (3 * a)) |^ 1) * ((b / (3 * a)) ^2)
.= ((b / (3 * a)) to_power 1) * ((b / (3 * a)) ^2) by POWER:41 ;
((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 A5, A6, A7, A8
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / ((3 * a) * a))) + (d / a)) by XCMPLX_1:76
.= (((- (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 A2, 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:76
.= ((((- (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:6
.= (((((- (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:6
.= ((((- (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:41
.= (((- (b / (3 * a))) * ((b / (3 * a)) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by POWER:25
.= (((- (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:76
.= (((- (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:76
.= (((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 A11, 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:76 ;
hence ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by A12, POWER:25; :: thesis: verum
end;
set p2 = ((3 * (h ^2)) + (2 * (a1 * h))) + a2;
A13: ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2)) / (3 * (a ^2))
proof
set t = ((3 * a) ") * b;
A14: (3 * a) / (3 * a) = 1 by A2, XCMPLX_1:60;
((3 * (h ^2)) + (2 * (a1 * h))) + a2 = ((3 * ((b / (3 * a)) ^2)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by A5
.= ((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:204
.= (((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:76
.= (((b ^2) / (3 * (a ^2))) - (2 * ((b / a) * (b / (3 * a))))) + (c / a) by A6, A7
.= (((b ^2) / (3 * (a ^2))) - (2 * ((b * b) / (a * (3 * a))))) + (c / a) by XCMPLX_1:76
.= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) / (3 * a)) * (c / a)) by A14
.= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) * c) / ((3 * a) * a)) by XCMPLX_1:76
.= (((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;
((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, A3, A4, A5, A6, A7, A8, Th15;
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 A6, A9, A13, A10; :: thesis: verum