let a, b, m be Nat; :: thesis: ( m > 0 implies ( a mod m = b mod m iff m divides a - b ) )

assume A1: m > 0 ; :: thesis: ( a mod m = b mod m iff m divides a - b )

thus ( a mod m = b mod m implies m divides a - b ) :: thesis: ( m divides a - b implies a mod m = b mod m )

then (a - b) mod m = 0 by A1, INT_1:62;

hence a mod m = b mod m by A1, Th22; :: thesis: verum

assume A1: m > 0 ; :: thesis: ( a mod m = b mod m iff m divides a - b )

thus ( a mod m = b mod m implies m divides a - b ) :: thesis: ( m divides a - b implies a mod m = b mod m )

proof

assume
m divides a - b
; :: thesis: a mod m = b mod m
assume
a mod m = b mod m
; :: thesis: m divides a - b

then (a - b) mod m = 0 by A1, Th22;

hence m divides a - b by A1, INT_1:62; :: thesis: verum

end;then (a - b) mod m = 0 by A1, Th22;

hence m divides a - b by A1, INT_1:62; :: thesis: verum

then (a - b) mod m = 0 by A1, INT_1:62;

hence a mod m = b mod m by A1, Th22; :: thesis: verum