let x, a, b, c be real number ; :: thesis: ( a <> 0 & delta a,b,c >= 0 implies ( ((a * (x ^2 )) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ) ) )
set lh = ((a * (x ^2 )) + (b * x)) + c;
set r1 = ((- b) - (sqrt (delta a,b,c))) / (2 * a);
set r2 = ((- b) + (sqrt (delta a,b,c))) / (2 * a);
assume that
A1: a <> 0 and
A2: delta a,b,c >= 0 ; :: thesis: ( ((a * (x ^2 )) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ) )
((a * (x ^2 )) + (b * x)) + c = (a * (x - (((- b) - (sqrt (delta a,b,c))) / (2 * a)))) * (x - (((- b) + (sqrt (delta a,b,c))) / (2 * a))) by A1, A2, QUIN_1:16;
hence ( ((a * (x ^2 )) + (b * x)) + c = 0 iff ( x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) ) ) by A1, A2, QUIN_1:15; :: thesis: verum