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 ^2 )) - 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 ^2 )) - q) mod (p |^ n) = 0
then p > 1 by INT_2:def 5;
then A3: p |^ n > 0 ;
given x being Integer such that A4: ((p * (x ^2 )) - q) mod (p |^ n) = 0 ; :: thesis: contradiction
(p * (x ^2 )) mod (p |^ n) = q mod (p |^ n) by A3, A4, Th22;
then p * ((x ^2 ) 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