let a, b, c, x be real number ; :: thesis: ( a <> 0 & delta a,b,c >= 0 & ((a * (x ^2 )) + (b * x)) + c = 0 & not x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) implies x = ((- b) + (sqrt (delta a,b,c))) / (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) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) )
A4: 2 * a <> 0 by A1;
((((2 * a) * x) + b) ^2 ) - (delta a,b,c) = 0 by A1, A3, Th14;
then (((2 * a) * x) + b) ^2 = (sqrt (delta a,b,c)) ^2 by A2, SQUARE_1:def 4;
then ( ((2 * a) * x) + b = sqrt (delta a,b,c) or ((2 * a) * x) + b = - (sqrt (delta a,b,c)) ) by Lm1;
hence ( x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ) by A4, XCMPLX_1:90; :: thesis: verum