let n, p, q be Nat; :: thesis: ( n > 0 & p > 0 implies (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) )
assume A1: ( n > 0 & p > 0 ) ; :: thesis: (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1)))
then A2: n >= 0 + 1 by NAT_1:13;
p * (q mod (p |^ (n -' 1))) = p * (q - ((q div (p |^ (n -' 1))) * (p |^ (n -' 1)))) by A1, NEWTON:77
.= (p * q) - ((q div (p |^ (n -' 1))) * (p * (p |^ (n -' 1))))
.= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ ((n -' 1) + 1))) by NEWTON:11
.= (p * q) - ((q div (p |^ (n -' 1))) * (p |^ n)) by A2, XREAL_1:237 ;
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 A1, NAT_D:1, XREAL_1:70;
then p * (q mod (p |^ (n -' 1))) < p |^ ((n -' 1) + 1) by NEWTON:11;
then p * (q mod (p |^ (n -' 1))) < p |^ n by A2, XREAL_1:237;
hence (p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1))) by A4, NAT_D:def 2; :: thesis: verum