let p, q, n be Nat; :: thesis: (p * q) mod (p * n) = p * (q mod n)

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

suppose A1: n = 0 ; :: thesis: (p * q) mod (p * n) = p * (q mod n)

then q mod n = 0 by NAT_D:def 2;
hence (p * q) mod (p * n) = p * (q mod n) by A1, NAT_D:def 2; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: (p * q) mod (p * n) = p * (q mod n)

then A3: p * q = p * ((n * (q div n)) + (q mod n)) by NAT_D:2
.= ((p * n) * (q div n)) + (p * (q mod n)) ;

per cases ( p = 0 or p > 0 ) ;

suppose p = 0 ; :: thesis: (p * q) mod (p * n) = p * (q mod n)

hence (p * q) mod (p * n) = p * (q mod n) by NAT_D:def 2; :: thesis: verum

end;

suppose p > 0 ; :: thesis: (p * q) mod (p * n) = p * (q mod n)

then p * (q mod n) < p * n by A2, NAT_D:1, XREAL_1:68;
hence (p * q) mod (p * n) = p * (q mod n) by A3, NAT_D:def 2; :: thesis: verum

end;

end;

end;

end;