let k, m, n be natural Number ; :: thesis: m mod n = ((n * k) + m) mod n

per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: m mod n = ((n * k) + m) mod n

for t being natural Number st m mod n = t holds
((n * k) + m) mod n = t

proof

let t be natural Number ; :: thesis: ( m mod n = t implies ((n * k) + m) mod n = t )
assume m mod n = t ; :: thesis: ((n * k) + m) mod n = t
then consider q being Nat such that
A2: m = (n * q) + t and
A3: t < n by A1, Def2;
A0: ( k is Nat & m is Nat & n is Nat & t is Nat ) by TARSKI:1;
ex p being Nat st
( (n * k) + m = (n * p) + t & t < n )

proof

reconsider p = k + q as Element of NAT by ORDINAL1:def 12;
take p ; :: thesis: ( (n * k) + m = (n * p) + t & t < n )
thus ( (n * k) + m = (n * p) + t & t < n ) by A2, A3; :: thesis: verum

end;

hence ((n * k) + m) mod n = t by A0, Def2; :: thesis: verum

end;

hence m mod n = ((n * k) + m) mod n ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: m mod n = ((n * k) + m) mod n

hence m mod n = ((n * k) + m) mod n ; :: thesis: verum

end;

end;