let a, b, c, x be Complex; :: thesis: ( a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 implies x = - (b / (2 * a)) )
assume that
A1: a <> 0 and
A2: delta (a,b,c) = 0 ; :: thesis: ( not Polynom (a,b,c,x) = 0 or x = - (b / (2 * a)) )
set y = x;
set t = ((a ^2) * (x ^2)) + ((a * b) * x);
A3: (b ^2) - ((4 * a) * c) = delta (a,b,c) by QUIN_1:def 1;
assume Polynom (a,b,c,x) = 0 ; :: thesis: x = - (b / (2 * a))
then a * (((a * (x ^2)) + (b * x)) + c) = 0 ;
then (((a ^2) * (x ^2)) + ((a * b) * x)) + (a * c) = 0 ;
then (((a * x) ^2) + (2 * (((a * x) * b) * (2 ")))) + ((b / 2) ^2) = 0 by A2, A3;
then ((a * x) + (b / 2)) ^2 = 0 ;
then (a * x) + (b / 2) = 0 by XCMPLX_1:6;
then x = (- (b * (2 "))) / a by A1, XCMPLX_1:89
.= ((- 1) * (b * (2 "))) * (a ") by XCMPLX_0:def 9
.= - ((b * ((2 ") * (a "))) * 1)
.= - (b * ((2 * a) ")) by XCMPLX_1:204 ;
hence x = - (b / (2 * a)) by XCMPLX_0:def 9; :: thesis: verum