let mlow, mhigh, f be Integer; :: thesis: ( mhigh < mlow + f & f > 0 implies ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) )
assume that
A1: mhigh < mlow + f and
A2: f > 0 ; :: thesis: ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f )
reconsider f = f as Element of NAT by A2, INT_1:3;
A3: mhigh + (- ((mhigh div f) * f)) < (mlow + f) + (- ((mhigh div f) * f)) by A1, XREAL_1:6;
A4: mhigh mod f = mhigh - ((mhigh div f) * f) by A2, INT_1:def 10;
then 0 <= mhigh - ((mhigh div f) * f) by A2, NAT_D:62;
then 0 + (- f) < ((mlow + (- ((mhigh div f) * f))) + f) + (- f) by A3, XREAL_1:6;
then - f < mlow - ((mhigh div f) * f) ;
hence ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) by A2, A4, NAT_D:62; :: thesis: verum