let a, b be Real; :: thesis: ( b > 0 implies ex r being Real st
( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b ) )
assume A1: b > 0 ; :: thesis: ex r being Real st
( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b )
set ab = [\(a / b)/];
set i = - [\(a / b)/];
take r = (b * (- [\(a / b)/])) + a; :: thesis: ( r = (b * (- [\(a / b)/])) + a & 0 <= r & r < b )
thus r = (b * (- [\(a / b)/])) + a ; :: thesis: ( 0 <= r & r < b )
[\(a / b)/] <= a / b by INT_1:def 6;
then [\(a / b)/] * b <= (a / b) * b by A1, XREAL_1:64;
then [\(a / b)/] * b <= a by A1, XCMPLX_1:87;
then - ([\(a / b)/] * b) >= - a by XREAL_1:24;
then (b * (- [\(a / b)/])) + a >= a + (- a) by XREAL_1:6;
hence 0 <= r ; :: thesis: r < b
(a / b) - 1 < [\(a / b)/] by INT_1:def 6;
then - ((a / b) - 1) > - [\(a / b)/] by XREAL_1:24;
then ((- (a / b)) + 1) * b > (- [\(a / b)/]) * b by A1, XREAL_1:68;
then (- ((a / b) * b)) + b > (- [\(a / b)/]) * b ;
then (- a) + b > (- [\(a / b)/]) * b by A1, XCMPLX_1:87;
then ((- a) + b) + a > r by XREAL_1:8;
hence r < b ; :: thesis: verum