let p be odd prime Nat; :: thesis: for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQf s) & j2 in rng (LAG4SQf 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 ;
A3: 2 * (p - s) = p - 1 by A1;
A4: p - 1 > 2 - 1 by lem3, XREAL_1:14;
A5: p - s > 0 by A3, A4;
A6: (p - s) + s > 0 + s by A5, XREAL_1:8;
A7: dom (LAG4SQf s) = Seg (len (LAG4SQf s)) by FINSEQ_1:def 3
.= Seg s by Def2 ;
for j1, j2 being Integer st j1 in rng (LAG4SQf s) & j2 in rng (LAG4SQf s) & j1 <> j2 holds
j1 mod p <> j2 mod p
proof
let j1, j2 be Integer; :: thesis: ( j1 in rng (LAG4SQf s) & j2 in rng (LAG4SQf s) & j1 <> j2 implies j1 mod p <> j2 mod p )
assume that
A8: j1 in rng (LAG4SQf s) and
A9: j2 in rng (LAG4SQf s) and
A10: j1 <> j2 ; :: thesis: j1 mod p <> j2 mod p
consider i1 being object such that
A11: i1 in dom (LAG4SQf s) and
A12: j1 = (LAG4SQf s) . i1 by A8, FUNCT_1:def 3;
consider i2 being object such that
A13: i2 in dom (LAG4SQf s) and
A14: j2 = (LAG4SQf s) . i2 by A9, FUNCT_1:def 3;
reconsider i1 = i1, i2 = i2 as Nat by A11, A13;
A15: j1 = (i1 - 1) ^2 by A11, A12, Def2;
A16: j2 = (i2 - 1) ^2 by A13, A14, Def2;
A17: j1 - j2 = ((i1 - 1) ^2) - ((i2 - 1) ^2) by A11, A12, A16, Def2
.= ((i1 + i2) - 2) * (i1 - i2) ;
A18: j2 - j1 = ((i2 - 1) ^2) - ((i1 - 1) ^2) by A11, A12, A16, Def2
.= ((i2 + i1) - 2) * (i2 - i1) ;
consider i9 being Nat such that
A19: i1 = i9 and
A20: 1 <= i9 and
A21: i9 <= s by A7, A11;
consider i0 being Nat such that
A22: i2 = i0 and
A23: 1 <= i0 and
A24: i0 <= s by A7, A13;
A25: (i1 + i2) - 2 < p
proof
A26: i1 + i2 <= s + s by A19, A21, A22, A24, XREAL_1:7;
(i1 + i2) + (- 2) < (p + 1) + (- 1) by A1, A26, XREAL_1:8;
hence (i1 + i2) - 2 < p ; :: thesis: verum
end;
A27: (i1 + i2) - 2 > 0
proof
per cases ( i2 = 1 or i2 > 1 ) by A22, A23, XXREAL_0:1;
suppose i2 = 1 ; :: thesis: (i1 + i2) - 2 > 0
then A29: i1 > 1 by A10, A12, A14, A19, A20, XXREAL_0:1;
A30: i1 + i2 > 1 + 1 by A22, A23, A29, XREAL_1:8;
(i1 + i2) + (- 2) > 2 + (- 2) by XREAL_1:8, A30;
hence (i1 + i2) - 2 > 0 ; :: thesis: verum
end;
suppose i2 > 1 ; :: thesis: (i1 + i2) - 2 > 0
then A32: i1 + i2 > 1 + 1 by A19, A20, XREAL_1:8;
(i1 + i2) + (- 2) > 2 + (- 2) by A32, XREAL_1:8;
hence (i1 + i2) - 2 > 0 ; :: thesis: verum
end;
end;
end;
A33: ( i1 - i2 < p & i2 - i1 < p )
proof
i1 - i2 <= i1 by XREAL_1:43;
then A34: i1 - i2 <= s by A19, A21, XXREAL_0:2;
i2 - i1 <= i2 by XREAL_1:43;
then i2 - i1 <= s by A22, A24, XXREAL_0:2;
hence ( i1 - i2 < p & i2 - i1 < p ) by A6, A34, XXREAL_0:2; :: thesis: verum
end;
j1 mod p <> j2 mod p
proof
per cases ( i1 > i2 or i2 > i1 ) by A10, A12, A14, XXREAL_0:1;
suppose i1 > i2 ; :: thesis: j1 mod p <> j2 mod p
then A39: i1 - i2 > 0 by XREAL_1:50;
reconsider i1 = i1, i2 = i2 as Nat ;
A40: (i1 + i2) - 2 in NAT by A27, INT_1:3;
A41: i1 - i2 in NAT by A39, INT_1:3;
(((i1 + i2) - 2) * (i1 - i2)) mod p <> 0
proof
assume (((i1 + i2) - 2) * (i1 - i2)) mod p = 0 ; :: thesis: contradiction
then A44: ((i1 + i2) - 2) * (i1 - i2) = (p * ((((i1 + i2) - 2) * (i1 - i2)) div p)) + 0 by A40, A41, NAT_D:2;
A45: (((i1 + i2) - 2) * (i1 - i2)) div p in NAT by A40, A41, INT_1:3, INT_1:55;
( p divides (i1 + i2) - 2 or p divides i1 - i2 ) by A40, A41, A44, A45, NEWTON:80, NAT_D:def 3;
hence contradiction by A25, A27, A33, A39, A40, A41, NAT_D:7; :: thesis: verum
end;
hence j1 mod p <> j2 mod p by A15, A16, A17, INT_4:22; :: thesis: verum
end;
suppose i2 > i1 ; :: thesis: j1 mod p <> j2 mod p
then A47: i2 - i1 > 0 by XREAL_1:50;
reconsider i1 = i1, i2 = i2 as Nat ;
reconsider p = p as Nat ;
A48: (i2 + i1) - 2 in NAT by A27, INT_1:3;
A49: i2 - i1 in NAT by A47, INT_1:3;
(((i2 + i1) - 2) * (i2 - i1)) mod p <> 0
proof
assume (((i2 + i1) - 2) * (i2 - i1)) mod p = 0 ; :: thesis: contradiction
then A52: ((i2 + i1) - 2) * (i2 - i1) = (p * ((((i2 + i1) - 2) * (i2 - i1)) div p)) + 0 by A48, A49, NAT_D:2;
A53: (((i2 + i1) - 2) * (i2 - i1)) div p in NAT by A48, A49, INT_1:3, INT_1:55;
( p divides (i2 + i1) - 2 or p divides i2 - i1 ) by A48, A49, A52, A53, NEWTON:80, NAT_D:def 3;
hence contradiction by A25, A27, A47, A33, A48, A49, NAT_D:7; :: thesis: verum
end;
hence j1 mod p <> j2 mod p by A15, A16, A18, INT_4:22; :: 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 (LAG4SQf s) & j2 in rng (LAG4SQf s) & not j1 = j2 holds
j1 mod p <> j2 mod p by A1; :: thesis: verum