let k, m, n be Nat; :: thesis: ( m <> 0 implies (k mod (m * n)) mod n = k mod n )
assume A1: m <> 0 ; :: thesis: (k mod (m * n)) mod n = k mod n
per cases ( n <> 0 or n = 0 ) ;
suppose A2: n <> 0 ; :: thesis: (k mod (m * n)) mod n = k mod n
reconsider k9 = k, m9 = m, n9 = n as Integer ;
m9 * n9 <> 0 by A1, A2, XCMPLX_1:6;
hence (k mod (m * n)) mod n = (k9 - ((k9 div (m9 * n9)) * (m9 * n9))) mod n9 by INT_1:def 10
.= (k9 + ((- (m9 * (k9 div (m9 * n9)))) * n9)) mod n9
.= k mod n by EULER_1:12 ;
:: thesis: verum
end;
suppose A3: n = 0 ; :: thesis: (k mod (m * n)) mod n = k mod n
hence (k mod (m * n)) mod n = 0 by NAT_D:def 2
.= k mod n by A3, NAT_D:def 2 ;
:: thesis: verum
end;
end;