let a, b, p, q be Real; :: thesis: ( a > 0 & p > 0 & (- b) / a < q / p implies ( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 ) )
assume A1: a > 0 ; :: thesis: ( not p > 0 or not (- b) / a < q / p or ( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 ) )
assume A2: p > 0 ; :: thesis: ( not (- b) / a < q / p or ( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 ) )
assume (- b) / a < q / p ; :: thesis: ( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 )
then A4a: ((- b) / a) - ((- b) / a) < (q / p) - ((- b) / a) by XREAL_1:9;
(q / p) - ((- b) / a) = ((q * a) - ((- b) * p)) / (p * a) by A1, A2, XCMPLX_1:130
.= ((q * a) + (b * p)) / (p * a) ;
then A5: (a * q) + (b * p) > 0 by A4a, A1, A2;
((q - b) / (a + p)) - ((- b) / a) = (((q - b) * a) - ((- b) * (a + p))) / ((a + p) * a) by XCMPLX_1:130, A1, A2
.= ((a * q) + (b * p)) / ((a + p) * a) ;
then A6: (((q - b) / (a + p)) - ((- b) / a)) + ((- b) / a) > 0 + ((- b) / a) by XREAL_1:6, A2, A1, A5;
((q - b) / (a + p)) - (q / p) = (((q - b) * p) - (q * (a + p))) / ((a + p) * p) by A1, XCMPLX_1:130, A2
.= (- ((a * q) + (b * p))) / ((a + p) * p) ;
then (((q - b) / (a + p)) - (q / p)) + (q / p) < 0 + (q / p) by XREAL_1:6, A1, A2, A5;
hence ( (- b) / a < (q - b) / (a + p) & (q - b) / (a + p) < q / p & ((a * q) + (b * p)) / (a + p) > 0 ) by A6, A5, A1, A2; :: thesis: verum