let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st 2 * n < n1 & n1 <= 4 * n & 2 * n < n2 & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n
let x, y be Integer; :: thesis: for a being non trivial Nat st 2 * n < n1 & n1 <= 4 * n & 2 * n < n2 & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n
let a be non trivial Nat; :: thesis: ( 2 * n < n1 & n1 <= 4 * n & 2 * n < n2 & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n implies n1, - n2 are_congruent_mod 2 * n )
assume that
A1: ( 2 * n < n1 & n1 <= 4 * n & 2 * n < n2 & n2 <= 4 * n ) and
A2: ( |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) ) ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )
reconsider m2 = n2 - (2 * n) as Nat by A1, NAT_1:21;
A3: m2 <= (4 * n) - (2 * n) by A1, XREAL_1:9;
( m2 > (2 * n) - (2 * n) & n2 > 0 ) by XREAL_1:9, A1;
then A4: ( sgn m2 = 1 & sgn n2 = 1 ) by ABSVALUE:def 2;
y <> 0 by A2, A1;
then ( y > 0 or y < 0 ) ;
then ( sgn y = 1 or sgn y = - 1 ) by ABSVALUE:def 2;
then A5: |.((sgn y) * (- (Py (a,m2)))).| = Py (a,m2) ;
reconsider m1 = n1 - (2 * n) as Nat by A1, NAT_1:21;
A6: m1 <= (4 * n) - (2 * n) by A1, XREAL_1:9;
( m1 > (2 * n) - (2 * n) & n1 > 0 ) by XREAL_1:9, A1;
then A7: ( sgn m1 = 1 & sgn n1 = 1 ) by ABSVALUE:def 2;
x <> 0 by A2, A1;
then ( x > 0 or x < 0 ) ;
then ( sgn x = 1 or sgn x = - 1 ) by ABSVALUE:def 2;
then A8: |.((sgn x) * (- (Py (a,m1)))).| = Py (a,m1) ;
(2 * n) + m1 = n1 ;
then (sgn n1) * (Py (a,|.n1.|)), - ((sgn m1) * (Py (a,|.m1.|))) are_congruent_mod Px (a,|.n.|) by Th30;
then (sgn x) * (Py (a,|.n1.|)),(sgn x) * (- (Py (a,m1))) are_congruent_mod Px (a,n) by A7, INT_4:11;
then x,(sgn x) * (- (Py (a,m1))) are_congruent_mod Px (a,n) by ABSVALUE:17, A2;
then (sgn x) * (- (Py (a,m1))),x are_congruent_mod Px (a,n) by INT_1:14;
then A9: (sgn x) * (- (Py (a,m1))),y are_congruent_mod Px (a,n) by INT_1:15, A2;
(2 * n) + m2 = n2 ;
then (sgn n2) * (Py (a,|.n2.|)), - ((sgn m2) * (Py (a,|.m2.|))) are_congruent_mod Px (a,|.n.|) by Th30;
then (sgn y) * (Py (a,|.n2.|)),(sgn y) * (- (Py (a,m2))) are_congruent_mod Px (a,n) by A4, INT_4:11;
then y,(sgn y) * (- (Py (a,m2))) are_congruent_mod Px (a,n) by ABSVALUE:17, A2;
then A10: (sgn x) * (- (Py (a,m1))),(sgn y) * (- (Py (a,m2))) are_congruent_mod Px (a,n) by A9, INT_1:15;

per cases ( m1 < m2 or m1 > m2 or m1 = m2 ) by XXREAL_0:1;

suppose ( m1 < m2 or m1 > m2 ) ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )

then ( m1 = (2 * n) - m2 or m2 = (2 * n) - m1 ) by A10, INT_1:14, A5, A3, A6, A8, Lm9;
then n1 - (- n2) = 3 * (2 * n) ;
hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by INT_1:def 5; :: thesis: verum

end;

suppose m1 = m2 ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )

then n1 - n2 = 0 * (2 * n) ;
hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by INT_1:def 5; :: thesis: verum

end;

end;