let a be non weightless Integer; :: thesis: for b being odd non weightless Integer st a,b are_coprime holds
(b + a) mod b <> (b - a) mod b
let b be odd non weightless Integer; :: thesis: ( a,b are_coprime implies (b + a) mod b <> (b - a) mod b )
assume A1: a,b are_coprime ; :: thesis: (b + a) mod b <> (b - a) mod b
A1a: not b divides a by A1, N0344;
then reconsider t = a mod b as non zero Integer by INT162;
A2: not b divides t by A1a, DIM;
A3: (b + a) mod b = ((b mod b) + (a mod b)) mod b by NAT_D:66
.= t mod b ;
A4: (b - a) mod b = ((b mod b) - (a mod b)) mod b by INT_6:7
.= (- t) mod b ;
( t mod b is odd iff (- t) mod b is even ) by A2, MOO;
hence (b + a) mod b <> (b - a) mod b by A3, A4; :: thesis: verum