let a, b, c be real number ; :: 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:93;
then 2 * (sqrt (delta a,b,c)) > 0 by XREAL_1:131;
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:61;
then A3: (- b) + (sqrt (delta a,b,c)) > (- b) + (- (sqrt (delta a,b,c))) by XREAL_1:8;
2 * a > 0 by A1, XREAL_1:131;
hence ((- b) + (sqrt (delta a,b,c))) / (2 * a) > ((- b) - (sqrt (delta a,b,c))) / (2 * a) by A3, XREAL_1:76; :: thesis: verum