let a, b, c, x be complex number ; :: thesis: ( a <> 0 & delta a,b,c = 0 & ((a * (x ^2 )) + (b * x)) + c = 0 implies x = - (b / (2 * a)) )
assume that
A1: a <> 0 and
A2: delta a,b,c = 0 and
A3: ((a * (x ^2 )) + (b * x)) + c = 0 ; :: thesis: x = - (b / (2 * a))
A4: 2 * a <> 0 by A1;
((((2 * a) * x) + b) ^2 ) - 0 = 0 by A1, A2, A3, Th14;
then ((2 * a) * x) + b = 0 by XCMPLX_1:6;
then x = (- b) / (2 * a) by A4, XCMPLX_1:90;
hence x = - (b / (2 * a)) by XCMPLX_1:188; :: thesis: verum