let a, n, r be Integer; :: thesis: ( 0 < n & 0 <= r & r < n & r <> (- a) mod n implies not n divides a + r )
set r1 = (- a) mod n;
assume that
A1: 0 < n and
A2: 0 <= r and
A3: r < n and
A4: r <> (- a) mod n and
A5: n divides a + r ; :: thesis: contradiction
A6: ( 0 <= (- a) mod n & (- a) mod n < n ) by A1, INT_1:57, INT_1:58;
then A7: ( n is Nat & r is Nat & (- a) mod n is Nat ) by A2, TARSKI:1;
(r - ((- a) mod n)) mod n = ((r mod n) - (((- a) mod n) mod n)) mod n by INT_6:7
.= (r - (- a)) mod n by INT_6:7
.= 0 by A1, A5, INT_1:62 ;
then n divides r - ((- a) mod n) by A1, INT_1:62;
hence contradiction by A3, A4, A6, A7, Th16; :: thesis: verum