let a, b, p, q, s be Real; ( a > 0 & p > 0 & (s - b) / a < (s - q) / (- p) implies ( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) ) )
assume AA:
a > 0
; ( not p > 0 or not (s - b) / a < (s - q) / (- p) or ( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) ) )
assume PP:
p > 0
; ( not (s - b) / a < (s - q) / (- p) or ( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) ) )
assume
(s - b) / a < (s - q) / (- p)
; ( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) )
then
((s - b) / a) * a < ((s - q) / (- p)) * a
by XREAL_1:68, AA;
then
(a / a) * (s - b) < ((s - q) / (- p)) * a
by XCMPLX_1:75;
then
1 * (s - b) < ((s - q) / (- p)) * a
by XCMPLX_1:60, AA;
then
(s - b) * (- p) > (((s - q) / (- p)) * a) * (- p)
by XREAL_1:69, PP;
then
(s - b) * (- p) > (((s - q) / (- p)) * (- p)) * a
;
then
((- p) * s) - (b * (- p)) > (s - q) * a
by XCMPLX_1:87, PP;
then
(((- p) * s) - (b * (- p))) + (p * s) > ((s * a) - (q * a)) + (p * s)
by XREAL_1:6;
then
(- (b * (- p))) + (a * q) > (((s * a) - (q * a)) + (p * s)) + (a * q)
by XREAL_1:6;
then
((b * p) + (a * q)) / (a + p) > (s * (a + p)) / (a + p)
by XREAL_1:74, AA, PP;
then A3:
((b * p) + (a * q)) / (a + p) > s
by XCMPLX_1:89, AA, PP;
(((b * p) + (a * q)) / (a + p)) - b =
(((b * p) + (a * q)) - (b * (a + p))) / (a + p)
by XCMPLX_1:126, AA, PP
.=
(a * (q - b)) / (a + p)
;
then
(a * (q - b)) / (a + p) > s - b
by A3, XREAL_1:9;
then
((a * (q - b)) / (a + p)) / a > (s - b) / a
by XREAL_1:74, AA;
then A4a:
(a * ((q - b) / (a + p))) / a > (s - b) / a
by XCMPLX_1:74;
(((b * p) + (a * q)) / (a + p)) - q =
(((b * p) + (a * q)) - (q * (a + p))) / (a + p)
by XCMPLX_1:126, AA, PP
.=
((- p) * (q - b)) / (a + p)
;
then
((- p) * (q - b)) / (a + p) > s - q
by XREAL_1:9, A3;
then
(((- p) * (q - b)) / (a + p)) / (- p) < (s - q) / (- p)
by XREAL_1:75, PP;
then
((- p) * ((q - b) / (a + p))) / (- p) < (s - q) / (- p)
by XCMPLX_1:74;
hence
( (s - b) / a < (q - b) / (a + p) & (q - b) / (a + p) < (s - q) / (- p) )
by PP, A4a, AA, XCMPLX_1:89; verum