let a, b be Integer; :: thesis: for c being odd Integer st (a + b) mod c = (a - b) mod c holds
c divides b
let c be odd Integer; :: thesis: ( (a + b) mod c = (a - b) mod c implies c divides b )
A1: 2 |^ 1,c are_coprime by NEWTON03:def 5;
assume (a + b) mod c = (a - b) mod c ; :: thesis: c divides b
then 0 mod c = (((a + b) mod c) - ((a - b) mod c)) mod c
.= ((a + b) - (a - b)) mod c by INT_6:7
.= (2 * b) mod c ;
hence c divides b by A1, INT_2:25, INT162; :: thesis: verum