let n, n1, n2 be Nat; 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; 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; ( 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) )
; ( 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;