let p, q, n be Nat; ( 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
; 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
; contradiction
per cases
( x >= 0 or x < 0 )
;
suppose
x < 0
;
contradictionthen
- 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;
verum end; end;