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) - 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) - q) mod (p |^ n) = 0

A4: p > 1 by A2, INT_2:def 4;

given x being Integer such that A5: ((p * x) - q) mod (p |^ n) = 0 ; :: thesis: contradiction

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) - q) mod (p |^ n) = 0

A4: p > 1 by A2, INT_2:def 4;

given x being Integer such that A5: ((p * x) - q) mod (p |^ n) = 0 ; :: thesis: contradiction

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

end;

suppose
x >= 0
; :: thesis: contradiction

then
x in NAT
by INT_1:3;

then reconsider x = x as Nat ;

(p * x) mod (p |^ n) = q mod (p |^ n) by A2, A5, Th22;

then p * (x 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

end;then reconsider x = x as Nat ;

(p * x) mod (p |^ n) = q mod (p |^ n) by A2, A5, Th22;

then p * (x 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

suppose
x < 0
; :: thesis: contradiction

then
- x in NAT
by INT_1:3;

then reconsider l = - x as Nat ;

A6: p divides p * l ;

p |^ n divides (p * x) - q by A2, A5, INT_1:62;

then p |^ n divides (- 1) * ((p * x) - q) by INT_2:2;

then consider k being Integer such that

A7: (p * l) + q = (p |^ n) * k ;

k >= 0 by A2, A7, XREAL_1:132;

then k in NAT by INT_1:3;

then reconsider k = k as Nat ;

(p * l) + q = (p |^ n) * k by A7;

then A8: p |^ n divides (p * l) + q ;

p divides p |^ n by A1, NAT_3:3;

then A9: p divides (p * l) + q by A8, NAT_D:4;

reconsider p = p, q = q as Element of NAT by ORDINAL1:def 12;

p gcd q > 1 by A4, A9, A6, NAT_D:10, NEWTON:49;

hence contradiction by A3, INT_2:def 3; :: thesis: verum

end;then reconsider l = - x as Nat ;

A6: p divides p * l ;

p |^ n divides (p * x) - q by A2, A5, INT_1:62;

then p |^ n divides (- 1) * ((p * x) - q) by INT_2:2;

then consider k being Integer such that

A7: (p * l) + q = (p |^ n) * k ;

k >= 0 by A2, A7, XREAL_1:132;

then k in NAT by INT_1:3;

then reconsider k = k as Nat ;

(p * l) + q = (p |^ n) * k by A7;

then A8: p |^ n divides (p * l) + q ;

p divides p |^ n by A1, NAT_3:3;

then A9: p divides (p * l) + q by A8, NAT_D:4;

reconsider p = p, q = q as Element of NAT by ORDINAL1:def 12;

p gcd q > 1 by A4, A9, A6, NAT_D:10, NEWTON:49;

hence contradiction by A3, INT_2:def 3; :: thesis: verum