set b1 = 1;
let a1, a2, a3, a4, a5, x1, x2, x3, x4 be Real; ( a1 <> 0 & ( for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) )
assume A1:
a1 <> 0
; ( ex x being Real st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) )
set b5 = ((x1 * x2) * x3) * x4;
set b4 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4));
set b3 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4);
set b2 = - (((x1 + x2) + x3) + x4);
assume A2:
for x being Real holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x)
; ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 )
now for x being Real holds Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x)let x be
Real;
Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x)set t =
((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4);
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
by A1, A2, Th11;
then ((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4) =
(a1 ") * ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + ((a3 * (x ^2)) + (a4 * x))) + a5)
by XCMPLX_0:def 9
.=
((((a1 ") * a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
.=
(((a1 / a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
by XCMPLX_0:def 9
.=
((1 * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
by A1, XCMPLX_1:60
.=
((x |^ 4) + (((a1 ") * a2) * (x |^ 3))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
.=
((x |^ 4) + ((a2 / a1) * (x |^ 3))) + (((((a1 ") * a3) * (x ^2)) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
by XCMPLX_0:def 9
.=
((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + (((a1 ") * a4) * x)) + ((a1 ") * a5))
by XCMPLX_0:def 9
.=
((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + ((a1 ") * a5))
by XCMPLX_0:def 9
.=
((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + (a5 / a1))
by XCMPLX_0:def 9
.=
Polynom (1,
(a2 / a1),
(a3 / a1),
(a4 / a1),
(a5 / a1),
x)
;
hence
Polynom (1,
(a2 / a1),
(a3 / a1),
(a4 / a1),
(a5 / a1),
x)
= Polynom (1,
(- (((x1 + x2) + x3) + x4)),
(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),
(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),
(((x1 * x2) * x3) * x4),
x)
;
verum end;
hence
( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 )
by Th9; verum