let p be Prime; :: thesis:
let a, m be Nat; :: thesis:
let f be FinSequence of NAT ; :: thesis:
assume A1: ( p > 2 & a gcd p = 1 & f = a * (idseq ((p -' 1) div 2)) & m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ) ; :: thesis:
then A2: a |^ ((p -' 1) div 2), Lege a,p are_congruent_mod p by Th28, INT_1:35;
set p' = (p -' 1) div 2;
set f1 = f mod p;
set f2 = Sgm (rng (f mod p));
set X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ;
A4: rng (idseq ((p -' 1) div 2)) = Seg ((p -' 1) div 2) by RELAT_1:71;
then reconsider I = idseq ((p -' 1) div 2) as FinSequence of NAT by FINSEQ_1:def 4;
dom f = dom I by A1, VALUED_1:def 5;
then A5: len f = len I by FINSEQ_3:31
.= (p -' 1) div 2 by FINSEQ_1:def 18 ;
(Product (f mod p)) mod p = (Product f) mod p by EULER_2:26;
then A6: Product (f mod p), Product f are_congruent_mod p by INT_3:12;
I is Element of ((p -' 1) div 2) -tuples_on NAT by FINSEQ_2:131;
then I is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:129;
then A7: Product f = (Product (((p -' 1) div 2) |-> a)) * (Product I) by A1, RVSUM_1:138
.= (a |^ ((p -' 1) div 2)) * (Product I) by NEWTON:def 1 ;
A8: p > 1 by INT_2:def 5;
then A9: p -' 1 = p - 1 by XREAL_1:235;
p >= 2 + 1 by A1, NAT_1:13;
then p - 1 >= 3 - 1 by XREAL_1:11;
then A10: (p -' 1) div 2 >= 1 by A9, NAT_2:15;
not p is even by A1, PEPIN:17;
then A11: p -' 1 is even by A9, HILBERT3:2;
then 2 divides p -' 1 by PEPIN:22;
then A12: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
then A13: (p -' 1) div 2 divides p -' 1 by NAT_D:def 3;
p -' 1 > 0 by A8, A9, XREAL_1:52;
then (p -' 1) div 2 <= p -' 1 by A13, NAT_D:7;
then A14: (p -' 1) div 2 < p by A9, XREAL_1:148, XXREAL_0:2;
A15: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by A11, NAT_2:28
.= p div 2 by A8, XREAL_1:237 ;
for d being Nat st d in dom I holds
(I . d) gcd p = 1

proof

let d be Nat; :: thesis:
assume d in dom I ; :: thesis:
then d in Seg (len I) by FINSEQ_1:def 3;
then A16: d in Seg ((p -' 1) div 2) by FINSEQ_1:def 18;
then A17: I . d = d by FINSEQ_2:57;
( d >= 1 & d <= (p -' 1) div 2 ) by A16, FINSEQ_1:3;
then ( d >= 1 & d < p ) by A14, XXREAL_0:2;
then d,p are_relative_prime by EULER_1:3;
hence (I . d) gcd p = 1 by A17, INT_2:def 4; :: thesis:

end;

then A18: (Product I) gcd p = 1 by WSIERP_1:43;
A19: for d being Nat st d in dom f holds
f . d = a * d

proof

let d be Nat; :: thesis:
assume A20: d in dom f ; :: thesis:
then d in dom I by A1, VALUED_1:def 5;
then d in Seg (len I) by FINSEQ_1:def 3;
then A21: d is Element of Seg ((p -' 1) div 2) by FINSEQ_1:def 18;
thus f . d = a * (I . d) by A1, A20, VALUED_1:def 5
.= a * d by A21, FINSEQ_2:57 ; :: thesis:

end;

A22: len (f mod p) = len f by EULER_2:def 1;
then A23: dom (f mod p) = dom f by FINSEQ_3:31;
f mod p <> {} by A5, A10, A22;
then rng (f mod p) is non empty Subset of NAT by FINSEQ_1:def 4;
then consider n1 being Element of NAT such that
A24: rng (f mod p) c= (Seg n1) \/ {0 } by HEYTING3:3;
not 0 in rng (f mod p)

proof

assume 0 in rng (f mod p) ; :: thesis:
then consider n being Nat such that
A25: ( n in dom (f mod p) & (f mod p) . n = 0 ) by FINSEQ_2:11;
reconsider a = a as Element of NAT by ORDINAL1:def 13;
0 = (f . n) mod p by A23, A25, EULER_2:def 1
.= (a * n) mod p by A19, A23, A25 ;
then A26: p divides a * n by PEPIN:6;
A27: ( n >= 1 & n <= (p -' 1) div 2 ) by A5, A22, A25, FINSEQ_3:27;
then p <= n by A1, A26, NAT_D:7, WSIERP_1:37;
hence contradiction by A14, A27, XXREAL_0:2; :: thesis:

end;

then A28: {0 } misses rng (f mod p) by ZFMISC_1:56;
then A29: rng (f mod p) c= Seg n1 by A24, XBOOLE_1:73;
then A30: rng (f mod p) = rng (Sgm (rng (f mod p))) by FINSEQ_1:def 13;
for x being set st x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } holds
x in rng (f mod p)

proof

let x be set ; :: thesis:
assume x in { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis:
then consider k being Element of NAT such that
A31: ( x = k & k in rng (f mod p) & k > p / 2 ) ;
thus x in rng (f mod p) by A31; :: thesis:

end;

then A32: { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } c= rng (f mod p) by TARSKI:def 3;
then reconsider X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } as finite set ;
A33: rng (f mod p) c= NAT by FINSEQ_1:def 4;
then reconsider X = X as finite Subset of NAT by A32, XBOOLE_1:1;
card X is Element of NAT ;
then reconsider m = m as Element of NAT by A1;
A34: (rng (f mod p)) \ X c= rng (f mod p) by XBOOLE_1:36;
then reconsider Y = (rng (f mod p)) \ X as finite Subset of NAT by A33, XBOOLE_1:1;
A35: for d, e being Element of NAT st 1 <= d & d < e & e <= len (f mod p) holds
(f mod p) . d <> (f mod p) . e

proof

let d, e be Element of NAT ; :: thesis:
assume A36: ( 1 <= d & d < e & e <= len (f mod p) ) ; :: thesis:
then ( 1 <= d & d < e & e <= len f ) by EULER_2:def 1;
then ( 1 <= d & d < len f & 1 <= e & e <= len f ) by XXREAL_0:2;
then A37: ( d in dom f & e in dom f ) by FINSEQ_3:27;
then A38: ( (f mod p) . d = (f . d) mod p & (f mod p) . e = (f . e) mod p ) by EULER_2:def 1;

now

assume (f mod p) . d = (f mod p) . e ; :: thesis:
then f . e,f . d are_congruent_mod p by A38, INT_3:12;
then p divides (f . e) - (f . d) by INT_2:19;
then p divides (a * e) - (f . d) by A19, A37;
then p divides (a * e) - (a * d) by A19, A37;
then A39: p divides a * (e - d) ;
reconsider dd = e - d as Element of NAT by A36, NAT_1:21;
A40: dd <> 0 by A36;
( abs p = p & abs dd = dd ) by ABSVALUE:def 1;
then A41: p <= dd by A1, A39, A40, INT_4:6, WSIERP_1:36;
A42: dd <= ((p -' 1) div 2) - 1 by A5, A22, A36, XREAL_1:15;
((p -' 1) div 2) - 1 < p by A14, XREAL_1:149;
hence contradiction by A41, A42, XXREAL_0:2; :: thesis:

end;

hence (f mod p) . d <> (f mod p) . e ; :: thesis:

end;

then A43: len f = card (rng (f mod p)) by A22, GRAPH_5:10;
card X <= card (rng (f mod p)) by A32, NAT_1:44;
then reconsider n = ((p -' 1) div 2) - m as Element of NAT by A1, A5, A43, NAT_1:21;
A44: len (f mod p) = card (rng (f mod p)) by A35, GRAPH_5:10;
then A45: f mod p is one-to-one by FINSEQ_4:77;
A46: Sgm (rng (f mod p)) is one-to-one by A24, A28, FINSEQ_3:99, XBOOLE_1:73;
then A47: Product (f mod p) = Product (Sgm (rng (f mod p))) by A30, A45, EULER_2:25, RFINSEQ:39;
A48: ( X c= Seg n1 & Y c= Seg n1 ) by A29, A32, A34, XBOOLE_1:1;

per cases ;

suppose A49: X is empty ; :: thesis:

for d being Nat st d in dom (f mod p) holds
( (f mod p) . d > 0 & (f mod p) . d <= (p -' 1) div 2 )

proof

let d be Nat; :: thesis:
assume A50: d in dom (f mod p) ; :: thesis:
reconsider d = d as Element of NAT by ORDINAL1:def 13;
reconsider f1 = f mod p as FinSequence of NAT ;
( f1 . d in rng f1 & not f1 . d in X ) by A49, A50, FUNCT_1:12;
then A51: f1 . d <= p / 2 ;
A52: f1 . d in rng f1 by A50, FUNCT_1:12;
then f1 . d in {0 } \/ (rng f1) by XBOOLE_0:def 3;
then not f1 . d in {0 } by A28, A52, XBOOLE_0:5;
then f1 . d <> 0 by TARSKI:def 1;
hence ( (f mod p) . d > 0 & (f mod p) . d <= (p -' 1) div 2 ) by A15, A51, INT_1:81; :: thesis:

end;

then rng (f mod p) = rng I by A4, A5, A22, A45, Th40;
then Product (f mod p) = Product I by A45, EULER_2:25, RFINSEQ:39;
then p divides (1 * (Product I)) - ((a |^ ((p -' 1) div 2)) * (Product I)) by A6, A7, INT_2:19;
then p divides (1 - (a |^ ((p -' 1) div 2))) * (Product I) ;
then p divides 1 - (a |^ ((p -' 1) div 2)) by A18, WSIERP_1:36;
then 1,a |^ ((p -' 1) div 2) are_congruent_mod p by INT_2:19;
then A53: 1, Lege a,p are_congruent_mod p by A2, INT_1:36;

now

assume Lege a,p = - 1 ; :: thesis:
then p divides 1 - (- 1) by A53, INT_2:19;
hence contradiction by A1, NAT_D:7; :: thesis:

end;

then Lege a,p = 1 by Th25;
hence Lege a,p = (- 1) |^ m by A1, A49, CARD_1:47, NEWTON:9; :: thesis:

end;

suppose not X is empty ; :: thesis:

A55: Sgm (rng (f mod p)) = (Sgm Y) ^ (Sgm X)

proof

for k, l being Element of NAT st k in Y & l in X holds
k < l

proof

let k, l be Element of NAT ; :: thesis:
assume A56: ( k in Y & l in X ) ; :: thesis:
then ( k in rng (f mod p) & not k in X ) by XBOOLE_0:def 5;
then A57: k <= p / 2 ;
ex l1 being Element of NAT st
( l1 = l & l1 in rng (f mod p) & l1 > p / 2 ) by A56;
hence k < l by A57, XXREAL_0:2; :: thesis:

end;

then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by A48, FINSEQ_3:48;
then Sgm ((rng (f mod p)) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;
hence Sgm (rng (f mod p)) = (Sgm Y) ^ (Sgm X) by A32, XBOOLE_1:12; :: thesis:

end;

A58: len (Sgm Y) = n

proof

len (Sgm Y) = card Y by A29, A34, FINSEQ_3:44, XBOOLE_1:1
.= ((p -' 1) div 2) - m by A1, A5, A22, A32, A44, CARD_2:63 ;
hence len (Sgm Y) = n ; :: thesis:

end;

then A59: (Sgm (rng (f mod p))) /^ n = Sgm X by A55, FINSEQ_5:40;
Sgm (rng (f mod p)) = ((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n) by RFINSEQ:21;
then A60: ( (Sgm (rng (f mod p))) | n is one-to-one & (Sgm (rng (f mod p))) /^ n is one-to-one ) by A46, FINSEQ_3:98;
A61: (Sgm (rng (f mod p))) | n = Sgm Y by A55, A58, FINSEQ_3:122, FINSEQ_6:12;
A63: len (Sgm (rng (f mod p))) = (p -' 1) div 2 by A5, A22, A24, A28, A44, FINSEQ_3:44, XBOOLE_1:73;
then A64: n <= len (Sgm (rng (f mod p))) by XREAL_1:45;
A65: len ((Sgm (rng (f mod p))) | n) = n by A63, FINSEQ_1:80, XREAL_1:45;
set f3 = ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n);
set f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n));
A66: dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = (dom ((len ((Sgm (rng (f mod p))) /^ n)) |-> p)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by VALUED_1:12
.= (Seg (len ((len ((Sgm (rng (f mod p))) /^ n)) |-> p))) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3
.= (Seg (len ((Sgm (rng (f mod p))) /^ n))) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 18
.= (dom ((Sgm (rng (f mod p))) /^ n)) /\ (dom ((Sgm (rng (f mod p))) /^ n)) by FINSEQ_1:def 3
.= dom ((Sgm (rng (f mod p))) /^ n) ;
then A67: len (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) = len ((Sgm (rng (f mod p))) /^ n) by FINSEQ_3:31;
A68: len ((Sgm (rng (f mod p))) /^ n) = (len (Sgm (rng (f mod p)))) -' n by RFINSEQ:42
.= (len (Sgm (rng (f mod p)))) - n by A63, XREAL_1:45, XREAL_1:235
.= m by A63 ;
A69: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds
(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d)

proof

let d be Nat; :: thesis:
assume A70: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis:
then A71: d in Seg (len ((Sgm (rng (f mod p))) /^ n)) by A66, FINSEQ_1:def 3;
((len ((Sgm (rng (f mod p))) /^ n)) |-> p) . d = p by A71, FINSEQ_2:71;
hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A70, VALUED_1:13; :: thesis:

end;

A72: for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds
( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 )

proof

let d be Nat; :: thesis:
assume A73: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis:
then A74: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A69;
reconsider w = (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d as Element of INT by INT_1:def 2;
(Sgm X) . d in rng (Sgm X) by A59, A66, A73, FUNCT_1:12;
then (Sgm X) . d in X by A48, FINSEQ_1:def 13;
then consider ll being Element of NAT such that
A75: ( ll = (Sgm X) . d & ll in rng (f mod p) & ll > p / 2 ) ;
A76: w < p - (p / 2) by A59, A74, A75, XREAL_1:12;
consider e being Nat such that
A77: ( e in dom (f mod p) & (f mod p) . e = ((Sgm (rng (f mod p))) /^ n) . d ) by A59, A75, FINSEQ_2:11;
((Sgm (rng (f mod p))) /^ n) . d = (f . e) mod p by A23, A77, EULER_2:def 1;
then ((Sgm (rng (f mod p))) /^ n) . d < p by NAT_D:1;
hence ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d <= (p -' 1) div 2 ) by A15, A74, A76, INT_1:81, XREAL_1:52; :: thesis:

end;

for d being Nat st d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) holds
(((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT

proof

let d be Nat; :: thesis:
assume d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis:
then ( (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) & (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d > 0 ) by A69, A72;
hence (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d in NAT by INT_1:16; :: thesis:

end;

then reconsider f3 = ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n) as FinSequence of NAT by FINSEQ_2:14;
for d, e being Element of NAT st 1 <= d & d < e & e <= len f3 holds
f3 . d <> f3 . e

proof

let d, e be Element of NAT ; :: thesis:
assume A78: ( 1 <= d & d < e & e <= len f3 ) ; :: thesis:
then ( 1 <= d & d < len f3 & 1 <= e & e <= len f3 ) by XXREAL_0:2;
then A79: ( d in dom f3 & e in dom f3 ) by FINSEQ_3:27;
then ( f3 . d = p - (((Sgm (rng (f mod p))) /^ n) . d) & f3 . e = p - (((Sgm (rng (f mod p))) /^ n) . e) ) by A69;
hence f3 . d <> f3 . e by A60, A66, A78, A79, FUNCT_1:def 8; :: thesis:

end;

then len f3 = card (rng f3) by GRAPH_5:10;
then A80: f3 is one-to-one by FINSEQ_4:77;
( (Sgm (rng (f mod p))) | n is FinSequence of NAT & f3 is FinSequence of NAT ) ;
then reconsider f4 = ((Sgm (rng (f mod p))) | n) ^ (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) as FinSequence of NAT by FINSEQ_1:96;
A81: len f4 = n + m by A65, A67, A68, FINSEQ_1:35
.= len f by A5 ;
rng ((Sgm (rng (f mod p))) | n) misses rng f3

proof

assume rng ((Sgm (rng (f mod p))) | n) meets rng f3 ; :: thesis:
then consider x being set such that
A82: ( x in rng ((Sgm (rng (f mod p))) | n) & x in rng f3 ) by XBOOLE_0:3;
rng ((Sgm (rng (f mod p))) | n) c= rng (Sgm (rng (f mod p))) by FINSEQ_5:21;
then consider d1 being Nat such that
A83: ( d1 in dom (f mod p) & (f mod p) . d1 = x ) by A30, A82, FINSEQ_2:11;
A84: x = (f . d1) mod p by A23, A83, EULER_2:def 1;
consider e being Nat such that
A85: ( e in dom f3 & f3 . e = x ) by A82, FINSEQ_2:11;
x = p - (((Sgm (rng (f mod p))) /^ n) . e) by A69, A85;
then x = p - ((Sgm (rng (f mod p))) . (e + n)) by A64, A66, A85, RFINSEQ:def 2;
then A86: ((f . d1) mod p) + ((Sgm (rng (f mod p))) . (e + n)) = p by A84;
e + n in dom (Sgm (rng (f mod p))) by A66, A85, FINSEQ_5:29;
then (Sgm (rng (f mod p))) . (e + n) in rng (f mod p) by A30, FUNCT_1:12;
then consider e1 being Nat such that
A87: ( e1 in dom (f mod p) & (f mod p) . e1 = (Sgm (rng (f mod p))) . (e + n) ) by FINSEQ_2:11;
A88: e1 in dom f by A22, A87, FINSEQ_3:31;
then ((f . d1) mod p) + ((f . e1) mod p) = p by A86, A87, EULER_2:def 1;
then (((f . d1) mod p) + ((f . e1) mod p)) mod p = 0 by NAT_D:25;
then ((f . d1) + (f . e1)) mod p = 0 by EULER_2:8;
then p divides (f . d1) + (f . e1) by PEPIN:6;
then p divides (d1 * a) + (f . e1) by A19, A23, A83;
then p divides (d1 * a) + (e1 * a) by A19, A88;
then A89: p divides (d1 + e1) * a ;
( d1 >= 1 & d1 <= (p -' 1) div 2 & e1 >= 1 & e1 <= (p -' 1) div 2 ) by A5, A22, A83, A87, FINSEQ_3:27;
then ( d1 + e1 >= 1 + 1 & d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) ) by XREAL_1:9;
then ( d1 + e1 > 0 & d1 + e1 < p ) by A9, A12, XREAL_1:148, XXREAL_0:2;
hence contradiction by A1, A89, NAT_D:7, WSIERP_1:37; :: thesis:

end;

then A90: f4 is one-to-one by A60, A80, FINSEQ_3:98;
for d being Nat st d in dom f4 holds
( f4 . d > 0 & f4 . d <= (p -' 1) div 2 )

proof

let d be Nat; :: thesis:
assume A91: d in dom f4 ; :: thesis:

per cases by A91, FINSEQ_1:38;

suppose A92: d in dom ((Sgm (rng (f mod p))) | n) ; :: thesis:

reconsider d = d as Element of NAT by ORDINAL1:def 13;
((Sgm (rng (f mod p))) | n) . d in rng (Sgm Y) by A61, A92, FUNCT_1:12;
then ((Sgm (rng (f mod p))) | n) . d in Y by A48, FINSEQ_1:def 13;
then A93: ( ((Sgm (rng (f mod p))) | n) . d in rng (f mod p) & not ((Sgm (rng (f mod p))) | n) . d in X ) by XBOOLE_0:def 5;
then ((Sgm (rng (f mod p))) | n) . d <= p / 2 ;
then A94: ((Sgm (rng (f mod p))) | n) . d <= (p -' 1) div 2 by A15, INT_1:81;
not ((Sgm (rng (f mod p))) | n) . d in {0 } by A28, A93, XBOOLE_0:3;
then ((Sgm (rng (f mod p))) | n) . d <> 0 by TARSKI:def 1;
then ((Sgm (rng (f mod p))) | n) . d > 0 ;
hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A92, A94, FINSEQ_1:def 7; :: thesis:

end;

suppose ex l being Nat st
( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ; :: thesis:

then consider l being Element of NAT such that
A95: ( l in dom f3 & d = (len ((Sgm (rng (f mod p))) | n)) + l ) ;
f4 . d = f3 . l by A95, FINSEQ_1:def 7;
hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A72, A95; :: thesis:

end;

then rng f4 = rng I by A4, A5, A81, A90, Th40;
then Product f4 = Product I by A90, EULER_2:25, RFINSEQ:39;
then A96: (Product ((Sgm (rng (f mod p))) | n)) * (Product f3) = Product I by RVSUM_1:127;
A97: ( f3 is FinSequence of INT & (Sgm (rng (f mod p))) /^ n is FinSequence of INT ) by FINSEQ_2:27, NUMBERS:17;
for d being Nat st d in dom f3 holds
f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p

proof

let d be Nat; :: thesis:
assume d in dom f3 ; :: thesis:
then (f3 . d) mod p = (p - (((Sgm (rng (f mod p))) /^ n) . d)) mod p by A69
.= ((1 * p) + (- (((Sgm (rng (f mod p))) /^ n) . d))) mod p
.= (- (((Sgm (rng (f mod p))) /^ n) . d)) mod p by EULER_1:13 ;
hence f3 . d, - (((Sgm (rng (f mod p))) /^ n) . d) are_congruent_mod p by INT_3:12; :: thesis:

end;

then Product f3,((- 1) |^ m) * (Product ((Sgm (rng (f mod p))) /^ n)) are_congruent_mod p by A67, A68, A97, Th33;
then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),(((- 1) |^ m) * (Product ((Sgm (rng (f mod p))) /^ n))) * (Product ((Sgm (rng (f mod p))) | n)) are_congruent_mod p by INT_4:11;
then (Product f3) * (Product ((Sgm (rng (f mod p))) | n)),((- 1) |^ m) * ((Product ((Sgm (rng (f mod p))) | n)) * (Product ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p ;
then Product I,((- 1) |^ m) * (Product (((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n))) are_congruent_mod p by A96, RVSUM_1:127;
then A98: Product I,((- 1) |^ m) * (Product (f mod p)) are_congruent_mod p by A47, RFINSEQ:21;
((- 1) |^ m) * (Product (f mod p)),((- 1) |^ m) * (Product f) are_congruent_mod p by A6, INT_4:11;
then Product I,(((- 1) |^ m) * (a |^ ((p -' 1) div 2))) * (Product I) are_congruent_mod p by A7, A98, INT_1:36;
then p divides (1 * (Product I)) - ((((- 1) |^ m) * (a |^ ((p -' 1) div 2))) * (Product I)) by INT_2:19;
then p divides (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) * (Product I) ;
then p divides 1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2))) by A18, WSIERP_1:36;
then p divides ((- 1) |^ m) * (1 - (((- 1) |^ m) * (a |^ ((p -' 1) div 2)))) by INT_2:12;
then A99: p divides ((- 1) |^ m) - ((((- 1) |^ m) * ((- 1) |^ m)) * (a |^ ((p -' 1) div 2))) ;
((- 1) |^ m) * ((- 1) |^ m) = (- 1) |^ (m + m) by NEWTON:13
.= (- 1) |^ (2 * m)
.= ((- 1) |^ 2) |^ m by NEWTON:14
.= (1 |^ 2) |^ m by WSIERP_1:2
.= (1 ^2 ) |^ m by NEWTON:100
.= 1 by NEWTON:15 ;
then (- 1) |^ m,a |^ ((p -' 1) div 2) are_congruent_mod p by A99, INT_2:19;
then A100: (- 1) |^ m, Lege a,p are_congruent_mod p by A2, INT_1:36;
abs ((- 1) |^ m) = 1 by SERIES_2:1;
then A101: ( (- 1) |^ m = 1 or - ((- 1) |^ m) = 1 ) by ABSVALUE:1;

per cases ) |^ m = 1 or (- 1) |^ m = - 1 ) by A101;

suppose A102: (- 1) |^ m = 1 ; :: thesis:

now

assume Lege a,p = - 1 ; :: thesis:
then p divides 1 - (- 1) by A100, A102, INT_2:19;
hence contradiction by A1, NAT_D:7; :: thesis:

end;

hence Lege a,p = (- 1) |^ m by A102, Th25; :: thesis:

end;

suppose A103: (- 1) |^ m = - 1 ; :: thesis:

now

assume Lege a,p = 1 ; :: thesis:
then p divides (- 1) - 1 by A100, A103, INT_2:19;
then p divides - 2 ;
then p divides 2 by INT_2:14;
hence contradiction by A1, NAT_D:7; :: thesis:

end;

hence Lege a,p = (- 1) |^ m by A103, Th25; :: thesis:

end;