let i1, i2, i3 be Integer; :: thesis: ( i2 > 0 & i3 >= 0 implies (i1 mod (i2 * i3)) mod i3 = i1 mod i3 )
assume that
A1: i2 > 0 and
A2: i3 >= 0 ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

per cases ( i3 > 0 or i3 = 0 ) by A2;

suppose i3 > 0 ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

then i2 * i3 <> 0 by A1, XCMPLX_1:6;
then (i1 mod (i2 * i3)) mod i3 = (i1 - ((i1 div (i2 * i3)) * (i2 * i3))) mod i3 by INT_1:def 10
.= (i1 + ((- (i2 * (i1 div (i2 * i3)))) * i3)) mod i3 ;
hence (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by NAT_D:61; :: thesis: verum

end;

suppose A3: i3 = 0 ; :: thesis: (i1 mod (i2 * i3)) mod i3 = i1 mod i3

then (i1 mod (i2 * i3)) mod i3 = 0 by INT_1:def 10;
hence (i1 mod (i2 * i3)) mod i3 = i1 mod i3 by A3, INT_1:def 10; :: thesis: verum

end;

end;