let a, b, c, x be Complex; :: 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 & ((a * (x ^2)) + (b * x)) + c = 0 ) ; :: thesis: x = - (b / (2 * a))

((((2 * a) * x) + b) ^2) - 0 = 0 by A1, A2, Th14;

then A3: ((2 * a) * x) + b = 0 by XCMPLX_1:6;

2 * a <> 0 by A1;

then x = (- b) / (2 * a) by A3, XCMPLX_1:89;

hence x = - (b / (2 * a)) by XCMPLX_1:187; :: thesis: verum

assume that

A1: a <> 0 and

A2: ( delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 ) ; :: thesis: x = - (b / (2 * a))

((((2 * a) * x) + b) ^2) - 0 = 0 by A1, A2, Th14;

then A3: ((2 * a) * x) + b = 0 by XCMPLX_1:6;

2 * a <> 0 by A1;

then x = (- b) / (2 * a) by A3, XCMPLX_1:89;

hence x = - (b / (2 * a)) by XCMPLX_1:187; :: thesis: verum