let x1, x2 be real number ; :: thesis: for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom a,b,c,x = Quard a,x1,x2,x ) holds
( b / a = - (x1 + x2) & c / a = x1 * x2 )
let a, b, c be complex number ; :: thesis: ( a <> 0 & ( for x being real number holds Polynom a,b,c,x = Quard a,x1,x2,x ) implies ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A1:
a <> 0
; :: thesis: ( ex x being real number st not Polynom a,b,c,x = Quard a,x1,x2,x or ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A2:
for x being real number holds Polynom a,b,c,x = Quard a,x1,x2,x
; :: thesis: ( b / a = - (x1 + x2) & c / a = x1 * x2 )
now let z be
real number ;
:: thesis: Polynom 1,(- (x1 + x2)),(x1 * x2),z = Polynom 1,(b / a),(c / a),zA3:
Polynom a,
b,
c,
z = Quard a,
x1,
x2,
z
by A2;
set h =
z - x1;
set t =
z - x2;
A4:
a * (((z - x1) * (z - x2)) - (z ^2 )) = (b * z) + c
by A3;
set e =
((z - x1) * (z - x2)) - (z ^2 );
((z - x1) * (z - x2)) - (z ^2 ) =
((b * z) + c) / a
by A1, A4, XCMPLX_1:90
.=
(a " ) * ((b * z) + c)
by XCMPLX_0:def 9
.=
((a " ) * (b * z)) + ((a " ) * c)
;
then
(((z * z) - (z * x2)) - (x1 * z)) + (x1 * x2) = ((z ^2 ) + (((a " ) * b) * z)) + ((a " ) * c)
;
then ((z ^2 ) - ((x1 + x2) * z)) + (x1 * x2) =
((z ^2 ) + ((b / a) * z)) + ((a " ) * c)
by XCMPLX_0:def 9
.=
((z ^2 ) + ((b / a) * z)) + (c / a)
by XCMPLX_0:def 9
;
hence
Polynom 1,
(- (x1 + x2)),
(x1 * x2),
z = Polynom 1,
(b / a),
(c / a),
z
;
:: thesis: verum end;
hence
( b / a = - (x1 + x2) & c / a = x1 * x2 )
by Th4; :: thesis: verum