let p, q, n be Nat; :: thesis: ( n > 0 & p is prime & p,q are_coprime implies for x being Integer holds not ((p * (x ^2)) - q) mod (p |^ n) = 0 )

assume that

A1: n > 0 and

A2: p is prime and

A3: p,q are_coprime ; :: thesis: for x being Integer holds not ((p * (x ^2)) - q) mod (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 A2, A4, Th22;

then p * ((x ^2) mod (p |^ (n -' 1))) = q mod (p |^ n) by A1, A2, Th19;

then p divides q mod (p |^ n) ;

hence contradiction by A1, A2, A3, Th21; :: thesis: verum

assume that

A1: n > 0 and

A2: p is prime and

A3: p,q are_coprime ; :: thesis: for x being Integer holds not ((p * (x ^2)) - q) mod (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 A2, A4, Th22;

then p * ((x ^2) mod (p |^ (n -' 1))) = q mod (p |^ n) by A1, A2, Th19;

then p divides q mod (p |^ n) ;

hence contradiction by A1, A2, A3, Th21; :: thesis: verum