let n be natural Number ; :: thesis: ( n > 0 implies for a being Integer holds
( a mod n >= 0 & a mod n < n ) )
assume A1: n > 0 ; :: thesis: for a being Integer holds
( a mod n >= 0 & a mod n < n )
let a be Integer; :: thesis: ( a mod n >= 0 & a mod n < n )
now :: thesis: ( 0 <= a mod n & not a mod n >= n )
a div n = [\(a / n)/] by INT_1:def 9;
then a div n <= a / n by INT_1:def 6;
then (a div n) * n <= (a / n) * n by XREAL_1:64;
then (a div n) * n <= (a * (n ")) * n by XCMPLX_0:def 9;
then (a div n) * n <= a * ((n ") * n) ;
then (a div n) * n <= a * 1 by A1, XCMPLX_0:def 7;
then ((a div n) * n) - ((a div n) * n) <= a - ((a div n) * n) by XREAL_1:9;
hence 0 <= a mod n by INT_1:def 10; :: thesis: not a mod n >= n
assume a mod n >= n ; :: thesis: contradiction
then a - ((a div n) * n) >= n by A1, INT_1:def 10;
then (a + (- ((a div n) * n))) + ((a div n) * n) >= n + ((a div n) * n) by XREAL_1:6;
then a - n >= (n + ((a div n) * n)) - n by XREAL_1:9;
then (a - n) * (n ") >= ((a div n) * n) * (n ") by XREAL_1:64;
then (a - n) * (n ") >= (a div n) * (n * (n ")) ;
then (a * (n ")) - (n * (n ")) >= (a div n) * 1 by A1, XCMPLX_0:def 7;
then (a * (n ")) - 1 >= a div n by A1, XCMPLX_0:def 7;
then A2: (a / n) - 1 >= a div n by XCMPLX_0:def 9;
a div n = [\(a / n)/] by INT_1:def 9;
hence contradiction by A2, INT_1:def 6; :: thesis: verum
end;
hence ( a mod n >= 0 & a mod n < n ) ; :: thesis: verum