let p, q, n be Nat; :: thesis: ( n > 0 implies ( (p - q) mod n = 0 iff p mod n = q mod n ) )
assume A1: n > 0 ; :: thesis: ( (p - q) mod n = 0 iff p mod n = q mod n )
thus ( (p - q) mod n = 0 implies p mod n = q mod n ) :: thesis: ( p mod n = q mod n implies (p - q) mod n = 0 )
proof
assume (p - q) mod n = 0 ; :: thesis: p mod n = q mod n
then n divides p - q by A1, INT_1:62;
then consider s being Integer such that
A2: n * s = p - q ;
per cases ( p > q or p = q or p < q ) by XXREAL_0:1;
suppose p > q ; :: thesis: p mod n = q mod n
then s > 0 by A2, XREAL_1:50;
then s in NAT by INT_1:3;
then reconsider s9 = s as Nat ;
p mod n = ((n * s9) + q) mod n by A2
.= q mod n by NAT_D:21 ;
hence p mod n = q mod n ; :: thesis: verum
end;
suppose p = q ; :: thesis: p mod n = q mod n
hence p mod n = q mod n ; :: thesis: verum
end;
suppose A3: p < q ; :: thesis: p mod n = q mod n
A4: q - p = n * (- s) by A2;
then - s > 0 by A3, XREAL_1:50;
then - s in NAT by INT_1:3;
then reconsider s9 = - s as Nat ;
q - p = n * s9 by A4;
then q mod n = ((n * s9) + p) mod n
.= p mod n by NAT_D:21 ;
hence p mod n = q mod n ; :: thesis: verum
end;
end;
end;
assume A5: p mod n = q mod n ; :: thesis: (p - q) mod n = 0
p = (n * (p div n)) + (p mod n) by A1, NAT_D:2
.= (n * (p div n)) + (q - (n * (q div n))) by A1, A5, NEWTON:63
.= q + (n * ((p div n) - (q div n))) ;
then n divides p - q ;
hence (p - q) mod n = 0 by A1, INT_1:62; :: thesis: verum