let n, a, k be Integer; :: thesis: ( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )

hereby :: thesis: (a + (n * k)) mod n = a mod n

assume A2: n <> 0 ; :: thesis: (a + (n * k)) div n = (a div n) + k
thus (a + (n * k)) div n = [\((a + (n * k)) / n)/] by INT_1:def 9
.= [\((a + (n * k)) * (n "))/] by XCMPLX_0:def 9
.= [\((a * (n ")) + ((n * (n ")) * k))/]
.= [\((a * (n ")) + (1 * k))/] by A2, XCMPLX_0:def 7
.= [\(a * (n "))/] + k by INT_1:28
.= [\(a / n)/] + k by XCMPLX_0:def 9
.= (a div n) + k by INT_1:def 9 ; :: thesis: verum

end;

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

suppose A3: n <> 0 ; :: thesis: (a + (n * k)) mod n = a mod n

hence (a + (n * k)) mod n = (a + (n * k)) - (((a div n) + k) * n) by A1, INT_1:def 10
.= a - ((a div n) * n)
.= a mod n by A3, INT_1:def 10 ;
:: thesis: verum

end;

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

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

end;

end;