let n be natural number ; :: thesis: ( n > 0 implies for a being Integer holds
( a mod n = 0 iff n divides a ) )
assume A1: n > 0 ; :: thesis: for a being Integer holds
( a mod n = 0 iff n divides a )
let a be Integer; :: thesis: ( a mod n = 0 iff n divides a )

A2: now

assume a mod n = 0 ; :: thesis: n divides a
then 0 = a - ((a div n) * n) by A1, Def8;
hence n divides a by Def9; :: thesis: verum

end;

now

assume n divides a ; :: thesis: a mod n = 0
then consider k being Integer such that
A3: n * k = a by Def9;
A4: a mod n = a - ((a div n) * n) by A1, Def8
.= a - ([\(a / n)/] * n) ;
A5: k <= a / n

proof

assume k > a / n ; :: thesis: contradiction
then k * n > (a / n) * n by A1, XREAL_1:70;
then k * n > (a * (n " )) * n by XCMPLX_0:def 9;
then k * n > a * ((n " ) * n) ;
then n * k > a * 1 by A1, XCMPLX_0:def 7;
hence contradiction by A3; :: thesis: verum

end;

(a / n) - 1 < k

proof

- n <> 0 by A1;
then (- n) + a < 0 + a by XREAL_1:8;
then ((- n) + a) * (n " ) < (n * k) * (n " ) by A1, A3, XREAL_1:70;
then ((- n) * (n " )) + (a * (n " )) < (n * k) * (n " ) ;
then ((- n) * (n " )) + (a / n) < (n * (n " )) * k by XCMPLX_0:def 9;
then ((- n) * (n " )) + (a / n) < 1 * k by A1, XCMPLX_0:def 7;
then (- (n * (n " ))) + (a / n) < k ;
then (- 1) + (a / n) < k by A1, XCMPLX_0:def 7;
hence (a / n) - 1 < k ; :: thesis: verum

end;

then [\(a / n)/] = k by A5, Def4;
hence a mod n = 0 by A3, A4; :: thesis: verum

end;

hence ( a mod n = 0 iff n divides a ) by A2; :: thesis: verum