let i, k, n be Integer; :: thesis: (i + (k * n)) mod n = i mod n

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

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

then (i + (k * n)) mod n = (i + (k * n)) - (((i + (k * n)) div n) * n) by INT_1:def 10
.= (i + (k * n)) - ([\((i + (k * n)) / n)/] * n) by INT_1:def 9
.= (i + (k * n)) - ([\((i / n) + ((k * n) / n))/] * n) by XCMPLX_1:62
.= (i + (k * n)) - ([\((i / n) + (k / (n / n)))/] * n) by XCMPLX_1:77
.= (i + (k * n)) - ([\((i / n) + (k / 1))/] * n) by A1, XCMPLX_1:60
.= (i + (k * n)) - (([\(i / n)/] + k) * n) by INT_1:28
.= i - ([\(i / n)/] * n)
.= i - ((i div n) * n) by INT_1:def 9
.= i mod n by A1, INT_1:def 10 ;
hence (i + (k * n)) mod n = i mod n ; :: thesis: verum

end;

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

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

end;

end;