let a, b, c be Real; :: thesis: ( a < 0 & delta (a,b,c) > 0 implies ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
assume that
A1: a < 0 and
A2: delta (a,b,c) > 0 ; :: thesis: ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
sqrt (delta (a,b,c)) > 0 by A2, SQUARE_1:25;
then 2 * (sqrt (delta (a,b,c))) > 0 by XREAL_1:129;
then (sqrt (delta (a,b,c))) + (sqrt (delta (a,b,c))) > 0 ;
then sqrt (delta (a,b,c)) > - (sqrt (delta (a,b,c))) by XREAL_1:59;
then A3: (- b) + (sqrt (delta (a,b,c))) > (- b) + (- (sqrt (delta (a,b,c)))) by XREAL_1:6;
2 * a < 0 by A1, XREAL_1:132;
hence ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by A3, XREAL_1:75; :: thesis: verum