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 )

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

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 A5:
p mod n = q mod n
; :: thesis: (p - q) mod n = 0
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 ;

end;then n divides p - q by A1, INT_1:62;

then consider s being Integer such that

A2: n * s = p - q ;

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