let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st n1 <= 2 * n & n2 <= 2 * 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 & n2 <= 2 * 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 & n2 <= 2 * 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 & n2 <= 2 * 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 )
( n1 = n2 or n1 > n2 or n1 < n2 ) by XXREAL_0:1;
then ( n1 = n2 or n1 = (2 * n) - n2 or n2 = (2 * n) - n1 ) by Lm9, A2, INT_1:14, A1;
then ( n1 - n2 = (2 * n) * 0 or n1 - (- n2) = (2 * n) * 1 or n1 - (- n2) = (2 * n) * (- 1) ) ;
hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by INT_1:def 5; :: thesis: verum