let i, k, p be Nat; :: thesis: ( i * p <> 0 & k mod (i * p) < p implies k mod (i * p) = k mod p )
assume that
A1: i * p <> 0 and
A2: k mod (i * p) < p ; :: thesis: k mod (i * p) = k mod p
set T = k mod (i * p);
consider n being Nat such that
A3: k = ((i * p) * n) + (k mod (i * p)) and
k mod (i * p) < i * p by A1, NAT_D:def 2;
k = (p * (i * n)) + (k mod (i * p)) by A3;
then k mod p = (k mod (i * p)) mod p by NAT_D:21
.= k mod (i * p) by A2, NAT_D:24 ;
hence k mod (i * p) = k mod p ; :: thesis: verum