let n be Integer; :: 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 :: thesis: ( n divides a implies a mod n = 0 )
A3: a mod n = a - ((a div n) * n) by A1, Def10
.= a - ([\(a / n)/] * n) ;
assume n divides a ; :: thesis: a mod n = 0
then consider k being Integer such that
A4: n * k = a ;
- n <> 0 by A1;
then (- n) + a < 0 + a by A1, XREAL_1:6;
then ((- n) + a) * (n ") < (n * k) * (n ") by A1, A4, XREAL_1:68;
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;
then A5: (a / n) - 1 < k ;
k <= a / n
proof
assume k > a / n ; :: thesis: contradiction
then k * n > (a / n) * n by A1, XREAL_1:68;
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 A4; :: thesis: verum
end;
then [\(a / n)/] = k by A5, Def6;
hence a mod n = 0 by A4, A3; :: thesis: verum
end;
now :: thesis: ( a mod n = 0 implies n divides a )
assume a mod n = 0 ; :: thesis: n divides a
then 0 = a - ((a div n) * n) by A1, Def10;
hence n divides a ; :: thesis: verum
end;
hence ( a mod n = 0 iff n divides a ) by A2; :: thesis: verum