let x, a, b, c be Real; :: 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