let n, p, q be Nat; :: thesis: ( n > 0 & p is prime & p,q are_relative_prime implies not p divides q mod (p |^ n) )
assume that
A1: n > 0 and
A2: p is prime and
A3: p,q are_relative_prime ; :: thesis: not p divides q mod (p |^ n)
n >= 0 + 1 by A1, NAT_1:13;
then p |^ 1 divides p |^ n by RADIX_1:6;
then p divides p |^ n by NEWTON:5;
then A4: p divides (p |^ n) * (q div (p |^ n)) by NAT_D:9;
q = ((p |^ n) * (q div (p |^ n))) + (q mod (p |^ n)) by A2, NAT_D:2;
hence not p divides q mod (p |^ n) by A2, A3, A4, Lm6, NAT_D:8; :: thesis: verum