let i, j, n be Nat; for a being non trivial Nat st Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & n < i & i <= 2 * n & n < j & j <= 2 * n holds
i = j
let a be non trivial Nat; ( Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & n < i & i <= 2 * n & n < j & j <= 2 * n implies i = j )
set P = Px (a,n);
assume A1:
( Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & n < i & i <= 2 * n & n < j & j <= 2 * n )
; i = j
then reconsider i2n = (2 * n) - i, j2n = (2 * n) - j as Nat by NAT_1:21;
A2:
Px (a,n), Px (a,n) are_congruent_mod Px (a,n)
by INT_1:11;
( (2 * n) + (- i2n) = i & (2 * n) + (- j2n) = j )
;
then A3:
( Px (a,|.i.|), - (Px (a,|.(- i2n).|)) are_congruent_mod Px (a,|.n.|) & Px (a,|.j.|), - (Px (a,|.(- j2n).|)) are_congruent_mod Px (a,|.n.|) )
by Th17;
then
( - (Px (a,i2n)), Px (a,i) are_congruent_mod Px (a,n) & Px (a,|.j.|), - (Px (a,|.(- j2n).|)) are_congruent_mod Px (a,n) )
by INT_1:14;
then
- (Px (a,i2n)), Px (a,j) are_congruent_mod Px (a,n)
by A1, INT_1:15;
then
- (Px (a,i2n)), - (Px (a,j2n)) are_congruent_mod Px (a,n)
by A3, INT_1:15;
then A4:
(- (Px (a,i2n))) + (Px (a,n)),(- (Px (a,j2n))) + (Px (a,n)) are_congruent_mod Px (a,n)
by A2, INT_1:16;
( (2 * n) - i <= (2 * n) - n & (2 * n) - j <= (2 * n) - n )
by A1, XREAL_1:15;
then reconsider Pi = (Px (a,n)) - (Px (a,i2n)), Pj = (Px (a,n)) - (Px (a,j2n)) as Nat by NAT_1:21, HILB10_1:10;
( Pi < (Px (a,n)) - 0 & Pj < (Px (a,n)) - 0 )
by XREAL_1:15;
then
Pi = Pj
by Lm7, A4;
then
i2n = j2n
by Th20;
hence
i = j
; verum