let n, p, q be Nat; :: thesis: ( n > 0 & p is prime & p,q are_relative_prime implies for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0 )
assume A1: ( n > 0 & p is prime & p,q are_relative_prime ) ; :: thesis: for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0
then A2: p > 1 by INT_2:def 5;
then A3: p |^ n > 0 ;
given x being Integer such that A4: ((p * x) - q) mod (p |^ n) = 0 ; :: thesis: contradiction

per cases ( x >= 0 or x < 0 ) ;

suppose x >= 0 ; :: thesis: contradiction

then x in NAT by INT_1:16;
then reconsider x = x as Nat ;
(p * x) mod (p |^ n) = q mod (p |^ n) by A3, A4, Th22;
then p * (x mod (p |^ (n -' 1))) = q mod (p |^ n) by A1, Th19;
then p divides q mod (p |^ n) by NAT_D:def 3;
hence contradiction by A1, Th21; :: thesis: verum

end;

suppose x < 0 ; :: thesis: contradiction

then - x > 0 by XREAL_1:60;
then - x in NAT by INT_1:16;
then reconsider l = - x as Nat ;
p |^ n divides (p * x) - q by A3, A4, INT_1:89;
then p |^ n divides (- 1) * ((p * x) - q) by INT_2:12;
then consider k being Integer such that
A5: (p * l) + q = (p |^ n) * k by INT_1:def 9;
k >= 0 by A2, A5, XREAL_1:134;
then k in NAT by INT_1:16;
then reconsider k = k as Nat ;
(p * l) + q = (p |^ n) * k by A5;
then A6: p |^ n divides (p * l) + q by NAT_D:def 3;
p divides p |^ n by A1, NAT_3:3;
then A7: p divides (p * l) + q by A6, NAT_D:4;
A8: p divides p * l by NAT_D:9;
reconsider p = p, q = q as Element of NAT by ORDINAL1:def 13;
p gcd q > 1 by A2, A7, A8, NAT_D:10, NEWTON:62;
hence contradiction by A1, INT_2:def 4; :: thesis: verum

end;

end;