let p be Prime; :: thesis: for fp being FinSequence of NAT st p > 2 & ( for d being Nat st d in dom fp holds

(fp . d) gcd p = 1 ) holds

ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

let fp be FinSequence of NAT ; :: thesis: ( p > 2 & ( for d being Nat st d in dom fp holds

(fp . d) gcd p = 1 ) implies ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) )

assume A1: p > 2 ; :: thesis: ( ex d being Nat st

( d in dom fp & not (fp . d) gcd p = 1 ) or ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) )

deffunc H_{1}( Nat) -> Integer = Lege ((fp . $1),p);

set k = (p -' 1) div 2;

assume A2: for d being Nat st d in dom fp holds

(fp . d) gcd p = 1 ; :: thesis: ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

set f = fp |^ ((p -' 1) div 2);

reconsider f = fp |^ ((p -' 1) div 2) as FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

consider fr being FinSequence such that

A3: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = H_{1}(d) ) )
from FINSEQ_1:sch 2();

for d being Nat st d in dom fr holds

fr . d in INT

A4: fp is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A5: len f = len fp by NAT_3:def 1;

for d being Nat st d in dom fr holds

fr . d,f . d are_congruent_mod p

(Product fp) gcd p = 1 by A2, WSIERP_1:36;

then Lege ((Product fp),p),(Product fp) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;

then Lege ((Product fp),p), Product f are_congruent_mod p by A4, NAT_3:15;

then Lege ((Product fp),p), Product fr are_congruent_mod p by A8, INT_1:15;

then A9: p divides (Lege ((Product fp),p)) - (Product fr) ;

take fr ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

A10: for d being Nat holds

( not d in dom fr or fr . d = 1 or fr . d = 0 or fr . d = - 1 )

(fp . d) gcd p = 1 ) holds

ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

let fp be FinSequence of NAT ; :: thesis: ( p > 2 & ( for d being Nat st d in dom fp holds

(fp . d) gcd p = 1 ) implies ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) )

assume A1: p > 2 ; :: thesis: ( ex d being Nat st

( d in dom fp & not (fp . d) gcd p = 1 ) or ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) )

deffunc H

set k = (p -' 1) div 2;

assume A2: for d being Nat st d in dom fp holds

(fp . d) gcd p = 1 ; :: thesis: ex fr being FinSequence of INT st

( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

set f = fp |^ ((p -' 1) div 2);

reconsider f = fp |^ ((p -' 1) div 2) as FinSequence of INT by FINSEQ_2:24, NUMBERS:17;

consider fr being FinSequence such that

A3: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = H

for d being Nat st d in dom fr holds

fr . d in INT

proof

then reconsider fr = fr as FinSequence of INT by FINSEQ_2:12;
let d be Nat; :: thesis: ( d in dom fr implies fr . d in INT )

assume d in dom fr ; :: thesis: fr . d in INT

then fr . d = Lege ((fp . d),p) by A3;

hence fr . d in INT by INT_1:def 2; :: thesis: verum

end;assume d in dom fr ; :: thesis: fr . d in INT

then fr . d = Lege ((fp . d),p) by A3;

hence fr . d in INT by INT_1:def 2; :: thesis: verum

A4: fp is FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

A5: len f = len fp by NAT_3:def 1;

for d being Nat st d in dom fr holds

fr . d,f . d are_congruent_mod p

proof

then A8:
Product f, Product fr are_congruent_mod p
by A3, A5, Th32, INT_1:14;
let d be Nat; :: thesis: ( d in dom fr implies fr . d,f . d are_congruent_mod p )

assume A6: d in dom fr ; :: thesis: fr . d,f . d are_congruent_mod p

then d in dom fp by A3, FINSEQ_3:29;

then (fp . d) gcd p = 1 by A2;

then Lege ((fp . d),p),(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;

then A7: fr . d,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A3, A6;

d in dom f by A3, A5, A6, FINSEQ_3:29;

hence fr . d,f . d are_congruent_mod p by A7, NAT_3:def 1; :: thesis: verum

end;assume A6: d in dom fr ; :: thesis: fr . d,f . d are_congruent_mod p

then d in dom fp by A3, FINSEQ_3:29;

then (fp . d) gcd p = 1 by A2;

then Lege ((fp . d),p),(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;

then A7: fr . d,(fp . d) |^ ((p -' 1) div 2) are_congruent_mod p by A3, A6;

d in dom f by A3, A5, A6, FINSEQ_3:29;

hence fr . d,f . d are_congruent_mod p by A7, NAT_3:def 1; :: thesis: verum

(Product fp) gcd p = 1 by A2, WSIERP_1:36;

then Lege ((Product fp),p),(Product fp) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;

then Lege ((Product fp),p), Product f are_congruent_mod p by A4, NAT_3:15;

then Lege ((Product fp),p), Product fr are_congruent_mod p by A8, INT_1:15;

then A9: p divides (Lege ((Product fp),p)) - (Product fr) ;

take fr ; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

A10: for d being Nat holds

( not d in dom fr or fr . d = 1 or fr . d = 0 or fr . d = - 1 )

proof

let d be Nat; :: thesis: ( not d in dom fr or fr . d = 1 or fr . d = 0 or fr . d = - 1 )

assume d in dom fr ; :: thesis: ( fr . d = 1 or fr . d = 0 or fr . d = - 1 )

then fr . d = Lege ((fp . d),p) by A3;

hence ( fr . d = 1 or fr . d = 0 or fr . d = - 1 ) by Th25; :: thesis: verum

end;assume d in dom fr ; :: thesis: ( fr . d = 1 or fr . d = 0 or fr . d = - 1 )

then fr . d = Lege ((fp . d),p) by A3;

hence ( fr . d = 1 or fr . d = 0 or fr . d = - 1 ) by Th25; :: thesis: verum

per cases
( Lege ((Product fp),p) = 1 or Lege ((Product fp),p) = 0 or Lege ((Product fp),p) = - 1 )
by Th25;

end;

suppose A11:
Lege ((Product fp),p) = 1
; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

then A12:
Product fr <> - 1
by A1, A9, NAT_D:7;

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A11, Th31, A12; :: thesis: verum

end;now :: thesis: not Product fr = 0

hence
( len fr = len fp & ( for d being Nat st d in dom fr holds assume
Product fr = 0
; :: thesis: contradiction

then p = 1 by A9, A11, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by A9, A11, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A11, Th31, A12; :: thesis: verum

suppose A13:
Lege ((Product fp),p) = 0
; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A13, Th31, A14; :: thesis: verum

end;

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

A14: now :: thesis: not Product fr = - 1

assume
Product fr = - 1
; :: thesis: contradiction

then p = 1 by A9, A13, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by A9, A13, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

now :: thesis: not Product fr = 1

hence
( len fr = len fp & ( for d being Nat st d in dom fr holds assume
Product fr = 1
; :: thesis: contradiction

then p divides 1 by A9, A13, INT_2:10;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p divides 1 by A9, A13, INT_2:10;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A13, Th31, A14; :: thesis: verum

suppose A15:
Lege ((Product fp),p) = - 1
; :: thesis: ( len fr = len fp & ( for d being Nat st d in dom fr holds

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A15, Th31, A16; :: thesis: verum

end;

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr )

A16: now :: thesis: not Product fr = 1

assume
Product fr = 1
; :: thesis: contradiction

then p divides - 2 by A9, A15;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

end;then p divides - 2 by A9, A15;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

now :: thesis: not Product fr = 0

hence
( len fr = len fp & ( for d being Nat st d in dom fr holds assume
Product fr = 0
; :: thesis: contradiction

then p divides 1 by A9, A15, INT_2:10;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p divides 1 by A9, A15, INT_2:10;

then p = 1 by WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

fr . d = Lege ((fp . d),p) ) & Lege ((Product fp),p) = Product fr ) by A3, A10, A15, Th31, A16; :: thesis: verum