let a, b, c, d, x1, x2, x3 be real number ; :: thesis: ( a <> 0 & ( for x being real number holds Polynom a,b,c,d,x = Tri a,x1,x2,x3,x ) implies ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
assume A1:
a <> 0
; :: thesis: ( ex x being real number st not Polynom a,b,c,d,x = Tri a,x1,x2,x3,x or ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
assume A2:
for x being real number holds Polynom a,b,c,d,x = Tri a,x1,x2,x3,x
; :: thesis: ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )
set b' = - ((x1 + x2) + x3);
set c' = ((x1 * x2) + (x2 * x3)) + (x1 * x3);
set d' = - ((x1 * x2) * x3);
set t1 = b / a;
set t2 = c / a;
set t3 = d / a;
now let x be
real number ;
:: thesis: Polynom 1,(b / a),(c / a),(d / a),x = Polynom 1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),xA3:
Polynom a,
b,
c,
d,
x = Tri a,
x1,
x2,
x3,
x
by A2;
set t =
(((a * (x |^ 3)) + (b * (x ^2 ))) + (c * x)) + d;
set r8 =
((x - x1) * (x - x2)) * (x - x3);
A4:
((((a * (x |^ 3)) + (b * (x ^2 ))) + (c * x)) + d) / a = ((x - x1) * (x - x2)) * (x - x3)
by A1, A3, XCMPLX_1:90;
A5:
x |^ 3 =
x |^ (2 + 1)
.=
(x |^ (1 + 1)) * x
by NEWTON:11
.=
((x |^ 1) * x) * x
by NEWTON:11
;
x |^ 1
= x to_power 1
by POWER:46;
then A6:
x |^ 3
= (x * x) * x
by A5, POWER:30;
(a " ) * ((((a * (x |^ 3)) + (b * (x ^2 ))) + (c * x)) + d) =
((((a " ) * a) * (x |^ 3)) + (((a " ) * b) * (x ^2 ))) + ((a " ) * ((c * x) + d))
.=
((1 * (x |^ 3)) + (((a " ) * b) * (x ^2 ))) + ((((a " ) * c) * x) + ((a " ) * d))
by A1, XCMPLX_0:def 7
.=
((1 * (x |^ 3)) + ((b / a) * (x ^2 ))) + ((((a " ) * c) * x) + ((a " ) * d))
by XCMPLX_0:def 9
.=
((1 * (x |^ 3)) + ((b / a) * (x ^2 ))) + (((c / a) * x) + ((a " ) * d))
by XCMPLX_0:def 9
.=
((1 * (x |^ 3)) + ((b / a) * (x ^2 ))) + (((c / a) * x) + (d / a))
by XCMPLX_0:def 9
.=
Polynom 1,
(b / a),
(c / a),
(d / a),
x
;
hence
Polynom 1,
(b / a),
(c / a),
(d / a),
x = Polynom 1,
(- ((x1 + x2) + x3)),
(((x1 * x2) + (x2 * x3)) + (x1 * x3)),
(- ((x1 * x2) * x3)),
x
by A4, A6, XCMPLX_0:def 9;
:: thesis: verum end;
hence
( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )
by Th12; :: thesis: verum