let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st n1 <= 2 * 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 n1 <= 2 * 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: ( n1 <= 2 * 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: ( n1 <= 2 * 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 m1 = n2 - (2 * n) as Nat by A1, NAT_1:21;
A3: m1 <= (4 * n) - (2 * n) by A1, XREAL_1:9;
( m1 > (2 * n) - (2 * n) & n2 > 0 ) by XREAL_1:9, A1;
then A4: ( sgn m1 = 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,m1)))).| = Py (a,m1) ;
(2 * n) + m1 = n2 ;
then (sgn n2) * (Py (a,|.n2.|)), - ((sgn m1) * (Py (a,|.m1.|))) are_congruent_mod Px (a,|.n.|) by Th30;
then (sgn y) * (Py (a,|.n2.|)),(sgn y) * (- (Py (a,m1))) are_congruent_mod Px (a,n) by A4, INT_4:11;
then y,(sgn y) * (- (Py (a,m1))) are_congruent_mod Px (a,n) by ABSVALUE:17, A2;
then A6: x,(sgn y) * (- (Py (a,m1))) are_congruent_mod Px (a,n) by INT_1:15, A2;

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

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

then ( n1 = (2 * n) - m1 or m1 = (2 * n) - n1 ) by A6, INT_1:14, A1, A2, A5, A3, Lm9;
then n1 - (- n2) = 2 * (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 n1 = m1 ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )

then n1 - n2 = (- 1) * (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;