let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st n1 < n2 & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
n1 = (2 * n) - n2
let x, y be Integer; :: thesis: for a being non trivial Nat st n1 < n2 & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) holds
n1 = (2 * n) - n2
let a be non trivial Nat; :: thesis: ( n1 < n2 & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) implies n1 = (2 * n) - n2 )
assume A1: ( n1 < n2 & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & n1 <> (2 * n) - n2 ) ; :: thesis: contradiction

per cases ( n2 <= n or n2 > n ) ;

suppose n2 <= n ; :: thesis: contradiction

then Py (a,n1) = Py (a,n2) by A1, Th33;
hence contradiction by A1, Th15; :: thesis: verum

end;

suppose A2: n2 > n ; :: thesis: contradiction

then reconsider m = n2 - n as Nat by NAT_1:21;
(n + n) - n2 >= n2 - n2 by A1, XREAL_1:9;
then reconsider nm = n - m as Element of NAT by INT_1:3;
A3: ( (sgn n2) * (Py (a,|.n2.|)) = Py (a,n2) & (sgn nm) * (Py (a,|.nm.|)) = Py (a,nm) ) by Th23;
n2 = n + m ;
then (sgn n2) * (Py (a,|.n2.|)),(sgn nm) * (Py (a,|.nm.|)) are_congruent_mod Px (a,|.n.|) by Th32;
then (sgn y) * (Py (a,n2)),(sgn y) * (Py (a,nm)) are_congruent_mod Px (a,n) by A3, INT_4:11;
then y,(sgn y) * (Py (a,nm)) are_congruent_mod Px (a,n) by A1, ABSVALUE:17;
then A4: x,(sgn y) * (Py (a,nm)) are_congruent_mod Px (a,n) by A1, INT_1:15;
then A5: (sgn y) * (Py (a,nm)),x are_congruent_mod Px (a,n) by INT_1:14;
nm = (n + n) - n2 ;
then A6: nm < (n + n) - n by A2, XREAL_1:15;
A7: ( n1 < nm or nm < n1 ) by A1, XXREAL_0:1;
y <> 0 by A1;
then ( y > 0 or y < 0 ) ;
then ( sgn y = 1 or sgn y = - 1 ) by ABSVALUE:def 2;
then ( (sgn y) * (Py (a,nm)) = Py (a,nm) or (sgn y) * (Py (a,nm)) = - (Py (a,nm)) ) ;
then A8: |.((sgn y) * (Py (a,nm))).| = Py (a,nm) ;

per cases ( n1 <= n or n1 > n ) ;

suppose n1 <= n ; :: thesis: contradiction

then A9: ( Py (a,n1) = Py (a,nm) or Py (a,n1) = - (Py (a,nm)) ) by A1, A4, INT_1:14, A8, A6, A7, Th33;
Py (a,n1) <> - (Py (a,nm))

proof

assume A10: Py (a,n1) = - (Py (a,nm)) ; :: thesis: contradiction
( n1 = 0 & nm = 0 ) by A10;
hence contradiction by A1; :: thesis: verum

end;

hence contradiction by A9, A1, Th15; :: thesis: verum

end;

suppose A11: n1 > n ; :: thesis: contradiction

then reconsider k = n1 - n as Nat by NAT_1:21;
n + n >= n1 by A1, XXREAL_0:2;
then (n + n) - n1 >= n1 - n1 by XREAL_1:9;
then reconsider nk = n - k as Element of NAT by INT_1:3;
A12: ( (sgn n1) * (Py (a,|.n1.|)) = Py (a,n1) & (sgn nk) * (Py (a,|.nk.|)) = Py (a,nk) ) by Th23;
n1 = n + k ;
then (sgn n1) * (Py (a,|.n1.|)),(sgn nk) * (Py (a,|.nk.|)) are_congruent_mod Px (a,|.n.|) by Th32;
then (sgn x) * (Py (a,n1)),(sgn x) * (Py (a,nk)) are_congruent_mod Px (a,n) by A12, INT_4:11;
then x,(sgn x) * (Py (a,nk)) are_congruent_mod Px (a,n) by A1, ABSVALUE:17;
then A13: (sgn y) * (Py (a,nm)),(sgn x) * (Py (a,nk)) are_congruent_mod Px (a,n) by A5, INT_1:15;
nk = (n + n) - n1 ;
then A14: nk < (n + n) - n by A11, XREAL_1:15;
A15: nk <> nm by A1;
then A16: ( nk < nm or nm < nk ) by XXREAL_0:1;
x <> 0 by A1, A11;
then ( x > 0 or x < 0 ) ;
then ( sgn x = 1 or sgn x = - 1 ) by ABSVALUE:def 2;
then ( (sgn x) * (Py (a,nk)) = Py (a,nk) or (sgn x) * (Py (a,nk)) = - (Py (a,nk)) ) ;
then A17: |.((sgn x) * (Py (a,nk))).| = Py (a,nk) ;
A18: ( Py (a,nk) = Py (a,nm) or Py (a,nk) = - (Py (a,nm)) ) by Th33, A16, A14, A6, A13, INT_1:14, A8, A17;
Py (a,nk) <> - (Py (a,nm))

proof

assume A19: Py (a,nk) = - (Py (a,nm)) ; :: thesis: contradiction
( nk = 0 & nm = 0 ) by A19;
hence contradiction by A1; :: thesis: verum

end;

hence contradiction by A18, A15, Th15; :: thesis: verum

end;

end;

end;

end;