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

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