let p be odd Prime; :: thesis: for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQg s) & j2 in rng (LAG4SQg s) & not j1 = j2 holds
j1 mod p <> j2 mod p
consider s being Integer such that
A1: p + 1 = 2 * s by ABIAN:11;
s > 0 by A1;
then s in NAT by INT_1:3;
then reconsider s = s as Nat ;
A4: 2 * (p - s) = p - 1 by A1;
p - 1 > 2 - 1 by lem3, XREAL_1:14;
then p - s > 0 by A4;
then A7: (p - s) + s > 0 + s by XREAL_1:8;
A8: dom (LAG4SQg s) = Seg (len (LAG4SQg s)) by FINSEQ_1:def 3
.= Seg s by Def3 ;
for j1, j2 being Integer st j1 in rng (LAG4SQg s) & j2 in rng (LAG4SQg s) & j1 <> j2 holds
j1 mod p <> j2 mod p

proof

let j1, j2 be Integer; :: thesis: ( j1 in rng (LAG4SQg s) & j2 in rng (LAG4SQg s) & j1 <> j2 implies j1 mod p <> j2 mod p )
assume that
A9: j1 in rng (LAG4SQg s) and
A10: j2 in rng (LAG4SQg s) and
A11: j1 <> j2 ; :: thesis: j1 mod p <> j2 mod p
consider i1 being object such that
A12: i1 in dom (LAG4SQg s) and
A13: j1 = (LAG4SQg s) . i1 by A9, FUNCT_1:def 3;
consider i2 being object such that
A14: i2 in dom (LAG4SQg s) and
A15: j2 = (LAG4SQg s) . i2 by A10, FUNCT_1:def 3;
reconsider i1 = i1, i2 = i2 as Nat by A12, A14;
A16: j2 = (- 1) - ((i2 - 1) ^2) by A14, A15, Def3;
A17: j2 - j1 = ((- 1) - ((i2 - 1) ^2)) - ((- 1) - ((i1 - 1) ^2)) by A12, A13, A16, Def3
.= ((i1 + i2) - 2) * (i1 - i2) ;
A18: j1 - j2 = ((- 1) - ((i1 - 1) ^2)) - ((- 1) - ((i2 - 1) ^2)) by A12, A13, A16, Def3
.= ((i2 + i1) - 2) * (i2 - i1) ;
consider i9 being Nat such that
A19: i1 = i9 and
A20: 1 <= i9 and
A21: i9 <= s by A8, A12;
consider i0 being Nat such that
A28: i2 = i0 and
A29: 1 <= i0 and
A30: i0 <= s by A8, A14;
A31: (i1 + i2) - 2 < p

proof

s + s = p + 1 by A1;
then i1 + i2 <= p + 1 by A19, A21, A28, A30, XREAL_1:7;
then (i1 + i2) + (- 2) < (p + 1) + (- 1) by XREAL_1:8;
hence (i1 + i2) - 2 < p ; :: thesis: verum

end;

A34: (i1 + i2) - 2 > 0

proof

per cases ( i2 = 1 or i2 > 1 ) by A28, A29, XXREAL_0:1;

suppose i2 = 1 ; :: thesis: (i1 + i2) - 2 > 0

then i1 > 1 by A11, A13, A15, A19, A20, XXREAL_0:1;
then i1 + i2 > 1 + 1 by A28, A29, XREAL_1:8;
then (i1 + i2) + (- 2) > 2 + (- 2) by XREAL_1:8;
hence (i1 + i2) - 2 > 0 ; :: thesis: verum

end;

suppose i2 > 1 ; :: thesis: (i1 + i2) - 2 > 0

then i1 + i2 > 1 + 1 by A19, A20, XREAL_1:8;
then (i1 + i2) + (- 2) > 2 + (- 2) by XREAL_1:8;
hence (i1 + i2) - 2 > 0 ; :: thesis: verum

end;

end;

end;

A40: ( i1 - i2 < p & i2 - i1 < p )

proof

i1 - i2 <= i1 by XREAL_1:43;
then A41: i1 - i2 <= s by A19, A21, XXREAL_0:2;
i2 - i1 <= i2 by XREAL_1:43;
then i2 - i1 <= s by A28, A30, XXREAL_0:2;
hence ( i1 - i2 < p & i2 - i1 < p ) by A7, A41, XXREAL_0:2; :: thesis: verum

end;

j1 mod p <> j2 mod p

proof

per cases ( i1 > i2 or i2 > i1 ) by A11, A13, A15, XXREAL_0:1;

suppose i1 > i2 ; :: thesis: j1 mod p <> j2 mod p

then A45: i1 - i2 > 0 by XREAL_1:50;
reconsider i1 = i1, i2 = i2 as Nat ;
reconsider p = p as Nat ;
A46: (i1 + i2) - 2 in NAT by A34, INT_1:3;
A47: i1 - i2 in NAT by A45, INT_1:3;
A48: (((i1 + i2) - 2) * (i1 - i2)) mod p <> 0

proof

assume A49: (((i1 + i2) - 2) * (i1 - i2)) mod p = 0 ; :: thesis: contradiction
A51: (((i1 + i2) - 2) * (i1 - i2)) div p in NAT by A46, A47, INT_1:3, INT_1:55;
((i1 + i2) - 2) * (i1 - i2) = (p * ((((i1 + i2) - 2) * (i1 - i2)) div p)) + 0 by A46, A47, A49, NAT_D:2;
then ( p divides (i1 + i2) - 2 or p divides i1 - i2 ) by A46, A47, A51, NAT_D:def 3, NEWTON:80;
hence contradiction by A31, A34, A40, A45, A46, A47, NAT_D:7; :: thesis: verum

end;

( j1 mod p = j2 mod p implies (j2 - j1) mod p = 0 )

proof

assume A53: j1 mod p = j2 mod p ; :: thesis: (j2 - j1) mod p = 0
(j2 - j1) mod p = ((j2 mod p) - (j1 mod p)) mod p by INT_6:7
.= 0 by NAT_D:26, A53 ;
hence (j2 - j1) mod p = 0 ; :: thesis: verum

end;

hence j1 mod p <> j2 mod p by A17, A48; :: thesis: verum

end;

suppose i2 > i1 ; :: thesis: j1 mod p <> j2 mod p

then A55: i2 - i1 > 0 by XREAL_1:50;
A56: (i2 + i1) - 2 in NAT by A34, INT_1:3;
A57: i2 - i1 in NAT by A55, INT_1:3;
A58: (((i2 + i1) - 2) * (i2 - i1)) mod p <> 0

proof

assume A59: (((i2 + i1) - 2) * (i2 - i1)) mod p = 0 ; :: thesis: contradiction
A61: (((i2 + i1) - 2) * (i2 - i1)) div p in NAT by A56, A57, INT_1:3, INT_1:55;
((i2 + i1) - 2) * (i2 - i1) = (p * ((((i2 + i1) - 2) * (i2 - i1)) div p)) + 0 by A56, A57, A59, NAT_D:2;
then ( p divides (i2 + i1) - 2 or p divides i2 - i1 ) by A56, A57, A61, NAT_D:def 3, NEWTON:80;
hence contradiction by A31, A34, A40, A55, A56, A57, NAT_D:7; :: thesis: verum

end;

( j1 mod p = j2 mod p implies (j1 - j2) mod p = 0 )

proof

assume A63: j1 mod p = j2 mod p ; :: thesis: (j1 - j2) mod p = 0
(j1 - j2) mod p = ((j1 mod p) - (j2 mod p)) mod p by INT_6:7
.= 0 by NAT_D:26, A63 ;
hence (j1 - j2) mod p = 0 ; :: thesis: verum

end;

hence j1 mod p <> j2 mod p by A18, A58; :: thesis: verum

end;

end;

end;

hence j1 mod p <> j2 mod p ; :: thesis: verum

end;

hence for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQg s) & j2 in rng (LAG4SQg s) & not j1 = j2 holds
j1 mod p <> j2 mod p by A1; :: thesis: verum