let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
x = y
let x, y be Integer; :: thesis: for a being non trivial Nat st n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
x = y
let a be non trivial Nat; :: thesis: ( n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) implies x = y )
assume A1: ( n1 < n2 & n2 <= n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) ) ; :: thesis: x = y
then consider i being Integer such that
A2: x - y = (Px (a,n)) * i by INT_1:def 5;
A3: n1 < n by A1, XXREAL_0:2;
( - (Px (a,n)) < x - y & x - y < Px (a,n) )

proof

per cases ( a = 2 or a <> 2 ) ;

suppose A4: a = 2 ; :: thesis: ( - (Px (a,n)) < x - y & x - y < Px (a,n) )

A5: (sqrt 3) ^2 = 3 by SQUARE_1:def 2;
A6: sqrt 3 > 0 by SQUARE_1:25;
(3 + (2 * (sqrt 3))) * (Py (a,n1)) < Px (a,n) by A4, A3, Th19;
then Py (a,n1) < (Px (a,n)) / (3 + (2 * (sqrt 3))) by A6, XREAL_1:81;
then A7: ( - ((Px (a,n)) / (3 + (2 * (sqrt 3)))) < x & x < (Px (a,n)) / (3 + (2 * (sqrt 3))) ) by Lm8, A1;
(sqrt 3) * (Py (a,n2)) < Px (a,n) by A4, Th18, A1;
then Py (a,n2) < (Px (a,n)) / (sqrt 3) by XREAL_1:81, A6;
then ( - ((Px (a,n)) / (sqrt 3)) < y & y < (Px (a,n)) / (sqrt 3) ) by Lm8, A1;
then A8: ( (- ((Px (a,n)) / (3 + (2 * (sqrt 3))))) - ((Px (a,n)) / (sqrt 3)) < x - y & x - y < ((Px (a,n)) / (3 + (2 * (sqrt 3)))) - (- ((Px (a,n)) / (sqrt 3))) ) by A7, XREAL_1:14;
A9: ((Px (a,n)) / (3 + (2 * (sqrt 3)))) + ((Px (a,n)) / (sqrt 3)) = (((Px (a,n)) * (sqrt 3)) + ((Px (a,n)) * (3 + (2 * (sqrt 3))))) / ((3 + (2 * (sqrt 3))) * (sqrt 3)) by XCMPLX_1:116, A6
.= ((Px (a,n)) * (3 + (3 * (sqrt 3)))) / ((3 + (2 * (sqrt 3))) * (sqrt 3))
.= (Px (a,n)) * ((3 + (3 * (sqrt 3))) / ((3 * (sqrt 3)) + 6)) by A5, XCMPLX_1:74 ;
3 + (3 * (sqrt 3)) <= 6 + (3 * (sqrt 3)) by XREAL_1:7;
then (3 + (3 * (sqrt 3))) / ((3 * (sqrt 3)) + 6) <= 1 by A6, XREAL_1:183;
then A10: (Px (a,n)) * ((3 + (3 * (sqrt 3))) / ((3 * (sqrt 3)) + 6)) <= (Px (a,n)) * 1 by XREAL_1:64;
then - (((Px (a,n)) / (3 + (2 * (sqrt 3)))) + ((Px (a,n)) / (sqrt 3))) >= - (Px (a,n)) by A9, XREAL_1:24;
hence ( - (Px (a,n)) < x - y & x - y < Px (a,n) ) by A10, A8, A9, XXREAL_0:2; :: thesis: verum

end;

suppose A11: a <> 2 ; :: thesis: ( - (Px (a,n)) < x - y & x - y < Px (a,n) )

2 * (Py (a,n1)) < Px (a,n) by A11, A3, Th17;
then |.x.| < (Px (a,n)) / 2 by A1, XREAL_1:81;
then A12: ( - ((Px (a,n)) / 2) < x & x < (Px (a,n)) / 2 ) by Lm8;
2 * (Py (a,n2)) < Px (a,n) by A11, Th17, A1;
then |.y.| < (Px (a,n)) / 2 by A1, XREAL_1:81;
then ( - ((Px (a,n)) / 2) < y & y < (Px (a,n)) / 2 ) by Lm8;
then ( (- ((Px (a,n)) / 2)) - ((Px (a,n)) / 2) < x - y & x - y < ((Px (a,n)) / 2) - (- ((Px (a,n)) / 2)) ) by A12, XREAL_1:14;
hence ( - (Px (a,n)) < x - y & x - y < Px (a,n) ) ; :: thesis: verum

end;

end;

end;

then ( (- 1) * (Px (a,n)) < (Px (a,n)) * i & (Px (a,n)) * i < 1 * (Px (a,n)) ) by A2;
then ( - 1 < i & i < 1 + 0 ) by XREAL_1:64;
then ( 0 <= i & i <= 0 ) by INT_1:7, INT_1:8;
then x - y = 0 by A2;
hence x = y ; :: thesis: verum