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_{1}( 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_{1}(d) ) )
from FINSEQ_1:sch 2();

for d being Nat st d in dom fp holds

fp . d in NAT

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

d gcd p = 1

(fp . d) gcd p = 1

(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

(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

( 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

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

for d being Nat st d in dom fp holds

fp . d in NAT

proof

then reconsider fp = fp as FinSequence of NAT by FINSEQ_2:12;
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;assume d in dom fp ; :: thesis: fp . d in NAT

then fp . d = d ^2 by A1;

hence fp . d in NAT ; :: thesis: verum

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

A19:
for d being Nat st d in dom fp holds
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;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

d gcd p = 1

proof

A23:
for d being Nat st d in dom fp holds
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;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

(fp . d) gcd p = 1

proof

take
fp
; :: thesis: ( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
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;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

(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

hence
( len fp = (p -' 1) div 2 & ( for d being Nat st d in dom fp holds
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;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

(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