let a, b, c, x be complex number ; :: thesis: ( a <> 0 & delta a,b,c = 0 & Polynom a,b,c,x = 0 implies x = - (b / (2 * a)) )
assume A1: ( a <> 0 & delta a,b,c = 0 ) ; :: thesis: ( not Polynom a,b,c,x = 0 or x = - (b / (2 * a)) )
set y = x;
assume Polynom a,b,c,x = 0 ; :: thesis: x = - (b / (2 * a))
then A2: a * (((a * (x ^2 )) + (b * x)) + c) = 0 ;
set t = ((a ^2 ) * (x ^2 )) + ((a * b) * x);
A3: (((a ^2 ) * (x ^2 )) + ((a * b) * x)) + (a * c) = 0 by A2;
(b ^2 ) - ((4 * a) * c) = delta a,b,c by QUIN_1:def 1;
then (((a * x) ^2 ) + (2 * (((a * x) * b) * (2 " )))) + ((b / 2) ^2 ) = 0 by A1, 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:90
.= ((- 1) * (b * (2 " ))) * (a " ) by XCMPLX_0:def 9
.= - ((b * ((2 " ) * (a " ))) * 1)
.= - (b * ((2 * a) " )) by XCMPLX_1:205 ;
hence x = - (b / (2 * a)) by XCMPLX_0:def 9; :: thesis: verum