let p, q, n be Nat; :: thesis: ( n > 0 & p > 0 implies (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) )
assume that
A1: n > 0 and
A2: p > 0 ; :: thesis: (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1)))
A3: n >= 0 + 1 by A1, NAT_1:13;
p * (q mod (p |^ (n -' 1))) = p * (q - ((q div (p |^ (n -' 1))) * (p |^ (n -' 1)))) by A2, NEWTON:63
.= (p * q) - ((q div (p |^ (n -' 1))) * (p * (p |^ (n -' 1))))
.= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ ((n -' 1) + 1))) by NEWTON:6
.= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ n)) by A3, XREAL_1:235 ;
then A4: p * q = ((q div (p |^ (n -' 1))) * (p |^ n)) + (p * (q mod (p |^ (n -' 1)))) ;
p * (q mod (p |^ (n -' 1))) < p * (p |^ (n -' 1)) by A2, NAT_D:1, XREAL_1:68;
then p * (q mod (p |^ (n -' 1))) < p |^ ((n -' 1) + 1) by NEWTON:6;
then p * (q mod (p |^ (n -' 1))) < p |^ n by A3, XREAL_1:235;
hence (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) by A4, NAT_D:def 2; :: thesis: verum