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