let m be Nat; :: thesis: for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
let z be Integer; :: thesis: ( 1 - m <= z & z <= m - 1 & m divides z implies z = 0 )
assume that
A1: 1 - m <= z and
A2: z <= m - 1 and
A3: m divides z ; :: thesis: z = 0
consider t being Integer such that
A4: z = m * t by A3, INT_1:def 3;
assume A5: z <> 0 ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( t > 0 or t < 0 ) by A5, A4;

suppose A6: t > 0 ; :: thesis: contradiction

then reconsider t = t as Element of NAT by INT_1:3;
m * t >= m by A6, NAT_1:14, NEWTON:33;
then (m * t) + 1 > m by NAT_1:13;
hence contradiction by A2, A4, XREAL_1:19; :: thesis: verum

end;

suppose A7: t < 0 ; :: thesis: contradiction

reconsider r = t + 1 as Integer ;
1 <= (m * t) + (m * 1) by A1, A4, XREAL_1:20;
then 1 <= m * (t + 1) ;
then 1 - 1 <= t by Th2, XREAL_1:20;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum