let p be Prime; :: thesis:
let a, m be Nat; :: thesis:
let f be FinSequence of NAT ; :: thesis:
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: f = a * (idseq ((p -' 1) div 2)) and
A4: m = card { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ; :: thesis:
set f1 = f mod p;
A5: len (f mod p) = len f by EULER_2:def 1;
set X = { k where k is Element of NAT : ( k in rng (f mod p) & k > p / 2 ) } ;
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 ex k being Element of NAT st
( x = k & k in rng (f mod p) & k > p / 2 ) ;
hence x in rng (f mod p) ; :: thesis:

end;

then A6: { 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 ;
A7: rng (f mod p) c= NAT by FINSEQ_1:def 4;
then reconsider X = X as finite Subset of NAT by A6, XBOOLE_1:1;
card X is Element of NAT ;
then reconsider m = m as Element of NAT by A4;
A8: (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 A7, XBOOLE_1:1;
A9: a |^ ((p -' 1) div 2), Lege (a,p) are_congruent_mod p by A1, A2, Th28, INT_1:35;
set f2 = Sgm (rng (f mod p));
(Product (f mod p)) mod p = (Product f) mod p by EULER_2:26;
then A10: Product (f mod p), Product f are_congruent_mod p by INT_3:12;
A11: p > 1 by INT_2:def 5;
then A12: p -' 1 = p - 1 by XREAL_1:235;
then A13: p -' 1 > 0 by A11, XREAL_1:52;
set p9 = (p -' 1) div 2;
A14: 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 A3, VALUED_1:def 5;
then A15: len f = len I by FINSEQ_3:31
.= (p -' 1) div 2 by FINSEQ_1:def 18 ;
p >= 2 + 1 by A1, NAT_1:13;
then p - 1 >= 3 - 1 by XREAL_1:11;
then f mod p <> {} by A15, A12, A5, NAT_2:15;
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
A16: rng (f mod p) c= (Seg n1) \/ {0} by HEYTING3:3;
I is Element of ((p -' 1) div 2) -tuples_on REAL by FINSEQ_2:129;
then A17: Product f = (Product (((p -' 1) div 2) |-> a)) * (Product I) by A3, RVSUM_1:138
.= (a |^ ((p -' 1) div 2)) * (Product I) by NEWTON:def 1 ;
not p is even by A1, PEPIN:17;
then A18: p -' 1 is even by A12, HILBERT3:2;
then A19: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by NAT_2:28
.= p div 2 by A11, XREAL_1:237 ;
2 divides p -' 1 by A18, PEPIN:22;
then A20: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
then (p -' 1) div 2 divides p -' 1 by NAT_D:def 3;
then (p -' 1) div 2 <= p -' 1 by A13, NAT_D:7;
then A21: (p -' 1) div 2 < p by A12, XREAL_1:148, XXREAL_0:2;
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 A22: d in Seg (len I) by FINSEQ_1:def 3;
then A23: d in Seg ((p -' 1) div 2) by FINSEQ_1:def 18;
then A24: I . d = d by FINSEQ_2:57;
d <= (p -' 1) div 2 by A23, FINSEQ_1:3;
then A25: d < p by A21, XXREAL_0:2;
d >= 1 by A22, FINSEQ_1:3;
then d,p are_relative_prime by A25, EULER_1:3;
hence (I . d) gcd p = 1 by A24, INT_2:def 4; :: thesis:

end;

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

proof

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

end;

A30: 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 that
A31: 1 <= d and
A32: d < e and
A33: e <= len (f mod p) ; :: thesis:
A34: e <= len f by A33, EULER_2:def 1;
1 <= e by A31, A32, XXREAL_0:2;
then A35: e in dom f by A34, FINSEQ_3:27;
then A36: (f mod p) . e = (f . e) mod p by EULER_2:def 1;
d < len f by A32, A34, XXREAL_0:2;
then A37: d in dom f by A31, FINSEQ_3:27;
then A38: (f mod p) . d = (f . d) 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, A36, INT_3:12;
then p divides (f . e) - (f . d) by INT_2:19;
then p divides (a * e) - (f . d) by A27, A35;
then p divides (a * e) - (a * d) by A27, A37;
then A39: p divides a * (e - d) ;
A40: ((p -' 1) div 2) - 1 < p by A21, XREAL_1:149;
reconsider dd = e - d as Element of NAT by A32, NAT_1:21;
A41: abs p = p by ABSVALUE:def 1;
A42: abs dd = dd by ABSVALUE:def 1;
A43: dd <= ((p -' 1) div 2) - 1 by A15, A5, A31, A33, XREAL_1:15;
dd <> 0 by A32;
then p <= dd by A2, A39, A41, A42, INT_4:6, WSIERP_1:36;
hence contradiction by A43, A40, XXREAL_0:2; :: thesis:

end;

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

end;

then A44: len (f mod p) = card (rng (f mod p)) by GRAPH_5:10;
then A45: f mod p is one-to-one by FINSEQ_4:77;
A46: dom (f mod p) = dom f by A5, FINSEQ_3:31;
not 0 in rng (f mod p)

proof

reconsider a = a as Element of NAT by ORDINAL1:def 13;
assume 0 in rng (f mod p) ; :: thesis:
then consider n being Nat such that
A47: n in dom (f mod p) and
A48: (f mod p) . n = 0 by FINSEQ_2:11;
0 = (f . n) mod p by A46, A47, A48, EULER_2:def 1
.= (a * n) mod p by A27, A46, A47 ;
then A49: p divides a * n by PEPIN:6;
n >= 1 by A47, FINSEQ_3:27;
then A50: p <= n by A2, A49, NAT_D:7, WSIERP_1:37;
n <= (p -' 1) div 2 by A15, A5, A47, FINSEQ_3:27;
hence contradiction by A21, A50, XXREAL_0:2; :: thesis:

end;

then A51: {0} misses rng (f mod p) by ZFMISC_1:56;
then A52: Sgm (rng (f mod p)) is one-to-one by A16, FINSEQ_3:99, XBOOLE_1:73;
A53: rng (f mod p) c= Seg n1 by A16, A51, XBOOLE_1:73;
then A54: X c= Seg n1 by A6, XBOOLE_1:1;
len f = card (rng (f mod p)) by A5, A30, GRAPH_5:10;
then reconsider n = ((p -' 1) div 2) - m as Element of NAT by A4, A15, A6, NAT_1:21, NAT_1:44;
A55: Y c= Seg n1 by A53, A8, XBOOLE_1:1;
A56: rng (f mod p) = rng (Sgm (rng (f mod p))) by A53, FINSEQ_1:def 13;
then A57: Product (f mod p) = Product (Sgm (rng (f mod p))) by A45, A52, EULER_2:25, RFINSEQ:39;
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));
A64: (Sgm (rng (f mod p))) /^ n is FinSequence of INT by FINSEQ_2:27, NUMBERS:17;
A65: 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 A66: 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;
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 that
A67: k in Y and
A68: l in X ; :: thesis:
A69: not k in X by A67, XBOOLE_0:def 5;
A70: ex l1 being Element of NAT st
( l1 = l & l1 in rng (f mod p) & l1 > p / 2 ) by A68;
k in rng (f mod p) by A67, XBOOLE_0:def 5;
then k <= p / 2 by A69;
hence k < l by A70, XXREAL_0:2; :: thesis:

end;

then Sgm (Y \/ X) = (Sgm Y) ^ (Sgm X) by A54, A55, FINSEQ_3:48;
then Sgm ((rng (f mod p)) \/ X) = (Sgm Y) ^ (Sgm X) by XBOOLE_1:39;
then A71: Sgm (rng (f mod p)) = (Sgm Y) ^ (Sgm X) by A6, XBOOLE_1:12;
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 = p - (((Sgm (rng (f mod p))) /^ n) . d)

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 d in Seg (len ((Sgm (rng (f mod p))) /^ n)) by A65, FINSEQ_1:def 3;
then ((len ((Sgm (rng (f mod p))) /^ n)) |-> p) . d = p by 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 A73, VALUED_1:13; :: thesis:

end;

A74: len (Sgm Y) = card Y by A53, A8, FINSEQ_3:44, XBOOLE_1:1
.= ((p -' 1) div 2) - m by A4, A15, A5, A6, A44, CARD_2:63 ;
then A75: (Sgm (rng (f mod p))) /^ n = Sgm X by A71, FINSEQ_5:40;
A76: 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:
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;
assume A77: d in dom (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) ; :: thesis:
then (Sgm X) . d in rng (Sgm X) by A75, A65, FUNCT_1:12;
then (Sgm X) . d in X by A54, FINSEQ_1:def 13;
then A78: ex ll being Element of NAT st
( ll = (Sgm X) . d & ll in rng (f mod p) & ll > p / 2 ) ;
then consider e being Nat such that
A79: e in dom (f mod p) and
A80: (f mod p) . e = ((Sgm (rng (f mod p))) /^ n) . d by A75, FINSEQ_2:11;
((Sgm (rng (f mod p))) /^ n) . d = (f . e) mod p by A46, A79, A80, EULER_2:def 1;
then A81: ((Sgm (rng (f mod p))) /^ n) . d < p by NAT_D:1;
A82: (((len ((Sgm (rng (f mod p))) /^ n)) |-> p) - ((Sgm (rng (f mod p))) /^ n)) . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A72, A77;
then w < p - (p / 2) by A75, A78, XREAL_1:12;
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 A19, A82, A81, 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 > 0 by A76;
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;
abs ((- 1) |^ m) = 1 by SERIES_2:1;
then A83: ( (- 1) |^ m = 1 or - ((- 1) |^ m) = 1 ) by ABSVALUE:1;
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;
A84: (Sgm (rng (f mod p))) | n = Sgm Y by A71, A74, FINSEQ_3:122, FINSEQ_6:12;
A85: 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 A86: d in dom f4 ; :: thesis:

per cases by A86, FINSEQ_1:38;

suppose A87: d in dom ((Sgm (rng (f mod p))) | n) ; :: 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
A91: l in dom f3 and
A92: d = (len ((Sgm (rng (f mod p))) | n)) + l ;
f4 . d = f3 . l by A91, A92, FINSEQ_1:def 7;
hence ( f4 . d > 0 & f4 . d <= (p -' 1) div 2 ) by A76, A91; :: thesis:

end;

A93: Sgm (rng (f mod p)) = ((Sgm (rng (f mod p))) | n) ^ ((Sgm (rng (f mod p))) /^ n) by RFINSEQ:21;
then A94: (Sgm (rng (f mod p))) /^ n is one-to-one by A52, FINSEQ_3:98;
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 that
A95: 1 <= d and
A96: d < e and
A97: e <= len f3 ; :: thesis:
1 <= e by A95, A96, XXREAL_0:2;
then A98: e in dom f3 by A97, FINSEQ_3:27;
then A99: f3 . e = p - (((Sgm (rng (f mod p))) /^ n) . e) by A72;
d < len f3 by A96, A97, XXREAL_0:2;
then A100: d in dom f3 by A95, FINSEQ_3:27;
then f3 . d = p - (((Sgm (rng (f mod p))) /^ n) . d) by A72;
hence f3 . d <> f3 . e by A94, A65, A96, A100, A98, A99, FUNCT_1:def 8; :: thesis:

end;

then len f3 = card (rng f3) by GRAPH_5:10;
then A101: f3 is one-to-one by FINSEQ_4:77;
A102: len (Sgm (rng (f mod p))) = (p -' 1) div 2 by A15, A5, A16, A51, A44, FINSEQ_3:44, XBOOLE_1:73;
then A103: n <= len (Sgm (rng (f mod p))) by XREAL_1:45;
A104: 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
A105: x in rng ((Sgm (rng (f mod p))) | n) and
A106: x in rng f3 by XBOOLE_0:3;
consider e being Nat such that
A107: e in dom f3 and
A108: f3 . e = x by A106, FINSEQ_2:11;
x = p - (((Sgm (rng (f mod p))) /^ n) . e) by A72, A107, A108;
then A109: x = p - ((Sgm (rng (f mod p))) . (e + n)) by A103, A65, A107, RFINSEQ:def 2;
e + n in dom (Sgm (rng (f mod p))) by A65, A107, FINSEQ_5:29;
then consider e1 being Nat such that
A110: e1 in dom (f mod p) and
A111: (f mod p) . e1 = (Sgm (rng (f mod p))) . (e + n) by A56, FINSEQ_2:11, FUNCT_1:12;
A112: e1 in dom f by A5, A110, FINSEQ_3:31;
A113: e1 <= (p -' 1) div 2 by A15, A5, A110, FINSEQ_3:27;
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
A114: d1 in dom (f mod p) and
A115: (f mod p) . d1 = x by A56, A105, FINSEQ_2:11;
d1 <= (p -' 1) div 2 by A15, A5, A114, FINSEQ_3:27;
then d1 + e1 <= ((p -' 1) div 2) + ((p -' 1) div 2) by A113, XREAL_1:9;
then A116: d1 + e1 < p by A12, A20, XREAL_1:148, XXREAL_0:2;
x = (f . d1) mod p by A46, A114, A115, EULER_2:def 1;
then ((f . d1) mod p) + ((Sgm (rng (f mod p))) . (e + n)) = p by A109;
then ((f . d1) mod p) + ((f . e1) mod p) = p by A111, A112, 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 A27, A46, A114;
then p divides (d1 * a) + (e1 * a) by A27, A112;
then A117: p divides (d1 + e1) * a ;
d1 >= 1 by A114, FINSEQ_3:27;
hence contradiction by A2, A117, A116, NAT_D:7, WSIERP_1:37; :: thesis:

end;

(Sgm (rng (f mod p))) | n is one-to-one by A52, A93, FINSEQ_3:98;
then A118: f4 is one-to-one by A101, A104, FINSEQ_3:98;
A119: 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 A72
.= ((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;

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

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

now

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

end;

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

end;

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

now

assume Lege (a,p) = 1 ; :: thesis:
then p divides (- 1) - 1 by A124, A126, 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 A126, Th25; :: thesis:

end;