let p be Prime; :: thesis: ( p > 2 implies ex fp being FinSequence of NAT st
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) ) )
deffunc H₁( Nat) -> Element of omega = $1 ^2 ;
consider fp being FinSequence such that
A1: ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
fp . d = H₁(d) ) ) from FINSEQ_1:sch 2();
for d being Nat st d in dom fp holds
fp . d in NAT

proof

let d be Nat; :: thesis: ( d in dom fp implies fp . d in NAT )
assume d in dom fp ; :: thesis: fp . d in NAT
then fp . d = d ^2 by A1;
hence fp . d in NAT ; :: thesis: verum

end;

then reconsider fp = fp as FinSequence of NAT by FINSEQ_2:12;
A2: p > 1 by INT_2:def 4;
then A3: p -' 1 = p - 1 by XREAL_1:233;
assume p > 2 ; :: thesis: ex fp being FinSequence of NAT st
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) )
then p is odd by PEPIN:17;
then p - 1 is even by HILBERT3:2;
then 2 divides p -' 1 by A3, PEPIN:22;
then (p -' 1) mod 2 = 0 by PEPIN:6;
then A4: (p -' 1) div 2 = (p -' 1) / 2 by PEPIN:63;
A5: for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p

proof

p - 1 > 0 by A2, XREAL_1:50;
then (p - 1) / 2 < (p - 1) / 1 by XREAL_1:76;
then (p -' 1) div 2 < p by A3, A4, XREAL_1:147;
then A6: ((p -' 1) div 2) - 1 < p by XREAL_1:147;
let d, e be Nat; :: thesis: ( d in dom fp & e in dom fp & d <> e implies not fp . d,fp . e are_congruent_mod p )
assume that
A7: d in dom fp and
A8: e in dom fp and
A9: d <> e ; :: thesis: not fp . d,fp . e are_congruent_mod p
A10: e in Seg ((p -' 1) div 2) by A1, A8, FINSEQ_1:def 3;
then A11: e <= (p -' 1) div 2 by FINSEQ_1:1;
A12: d in Seg ((p -' 1) div 2) by A1, A7, FINSEQ_1:def 3;
then A13: d >= 1 by FINSEQ_1:1;
then 1 - ((p -' 1) div 2) <= d - e by A11, XREAL_1:13;
then A14: - (((p -' 1) div 2) - 1) <= d - e ;
A15: d <= (p -' 1) div 2 by A12, FINSEQ_1:1;
then d + e <= ((p -' 1) div 2) + ((p -' 1) div 2) by A11, XREAL_1:7;
then d + e < p by A3, A4, XREAL_1:147;
then d + e,p are_coprime by A13, EULER_1:2;
then A16: (d + e) gcd p = 1 by INT_2:def 3;
assume fp . d,fp . e are_congruent_mod p ; :: thesis: contradiction
then p divides (d ^2) - (fp . e) by A1, A7;
then p divides (d ^2) - (e ^2) by A1, A8;
then A17: p divides (d - e) * (d + e) ;
d - e <> 0 by A9;
then |.p.| <= |.(d - e).| by A16, A17, INT_4:6, WSIERP_1:29;
then A18: p <= |.(d - e).| by ABSVALUE:def 1;
e >= 1 by A10, FINSEQ_1:1;
then d - e <= ((p -' 1) div 2) - 1 by A15, XREAL_1:13;
then |.(d - e).| <= ((p -' 1) div 2) - 1 by A14, ABSVALUE:5;
hence contradiction by A18, A6, XXREAL_0:2; :: thesis: verum

end;

A19: for d being Nat st d in dom fp holds
d gcd p = 1

proof

let d be Nat; :: thesis: ( d in dom fp implies d gcd p = 1 )
A20: 1 * d <= 2 * d by XREAL_1:64;
assume d in dom fp ; :: thesis: d gcd p = 1
then A21: d in Seg ((p -' 1) div 2) by A1, FINSEQ_1:def 3;
then d <= (p -' 1) div 2 by FINSEQ_1:1;
then 2 * d <= ((p -' 1) / 2) * 2 by A4, XREAL_1:64;
then d <= p -' 1 by A20, XXREAL_0:2;
then A22: d < p by A3, XREAL_1:147;
d >= 1 by A21, FINSEQ_1:1;
then d,p are_coprime by A22, EULER_1:2;
hence d gcd p = 1 by INT_2:def 3; :: thesis: verum

end;

A23: for d being Nat st d in dom fp holds
(fp . d) gcd p = 1

proof

let d be Nat; :: thesis: ( d in dom fp implies (fp . d) gcd p = 1 )
assume A24: d in dom fp ; :: thesis: (fp . d) gcd p = 1
then d gcd p = 1 by A19;
then (d ^2) gcd p = 1 by WSIERP_1:7;
hence (fp . d) gcd p = 1 by A1, A24; :: thesis: verum

end;

take fp ; :: thesis: ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) )
for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p

proof

let d be Nat; :: thesis: ( d in dom fp implies fp . d is_quadratic_residue_mod p )
assume A25: d in dom fp ; :: thesis: fp . d is_quadratic_residue_mod p
d ^2 is_quadratic_residue_mod p by Th9;
hence fp . d is_quadratic_residue_mod p by A1, A25; :: thesis: verum

end;

hence ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
(fp . d) gcd p = 1 ) & ( for d being Nat st d in dom fp holds
fp . d is_quadratic_residue_mod p ) & ( for d, e being Nat st d in dom fp & e in dom fp & d <> e holds
not fp . d,fp . e are_congruent_mod p ) ) by A1, A23, A5; :: thesis: verum