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

now

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

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

then reconsider t = t as Element of NAT by INT_1:16;
m * t >= m by A5, NAT_1:14, NEWTON:45;
then (m * t) + 1 > m by NAT_1:13;
hence contradiction by A1, A3, XREAL_1:21; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum