let p be Prime; :: thesis:
set p9 = (p -' 1) div 2;
set I = idseq ((p -' 1) div 2);
set fp = 2 * (idseq ((p -' 1) div 2));
set nn = p div 8;
A1: p > 1 by INT_2:def 5;
then A2: p - 1 = p -' 1 by XREAL_1:235;
A3: for d being Nat st d in dom (2 * (idseq ((p -' 1) div 2))) holds
(2 * (idseq ((p -' 1) div 2))) . d = 2 * d

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

end;

for d being Nat st d in dom (2 * (idseq ((p -' 1) div 2))) holds
(2 * (idseq ((p -' 1) div 2))) . d in NAT

proof

let d be Nat; :: thesis:
assume d in dom (2 * (idseq ((p -' 1) div 2))) ; :: thesis:
then (2 * (idseq ((p -' 1) div 2))) . d = 2 * d by A3;
hence (2 * (idseq ((p -' 1) div 2))) . d in NAT ; :: thesis:

end;

then reconsider fp = 2 * (idseq ((p -' 1) div 2)) as FinSequence of NAT by FINSEQ_2:14;
set f = fp mod p;
set X = { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ;
set m = card { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ;
dom fp = dom (idseq ((p -' 1) div 2)) by VALUED_1:def 5;
then A6: len fp = len (idseq ((p -' 1) div 2)) by FINSEQ_3:31
.= (p -' 1) div 2 by FINSEQ_1:def 18 ;
set Y = { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } ;
for x being set st x in { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } holds
x in dom (fp mod p)

proof

let x be set ; :: thesis:
assume x in { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } ; :: thesis:
then ex k being Element of NAT st
( x = k & k in dom (fp mod p) & (fp mod p) . k > p / 2 ) ;
hence x in dom (fp mod p) ; :: thesis:

end;

then { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } c= dom (fp mod p) by TARSKI:def 3;
then reconsider Y = { d where d is Element of NAT : ( d in dom (fp mod p) & (fp mod p) . d > p / 2 ) } as finite Subset of NAT by XBOOLE_1:1;
set Z = seq (p div 4),(((p -' 1) div 2) -' (p div 4));
A7: p mod 8 <= 8 - 1 by INT_1:79, NAT_D:1;
8 = 2 * 4 ;
then A8: 2 divides 8 by NAT_D:def 3;

A9: now

assume p mod 8 = 0 ; :: thesis:
then 8 divides p by PEPIN:6;
then p = 8 by INT_2:def 5;
hence contradiction by A8, NAT_4:12; :: thesis:

end;

for x being set st x in { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } holds
x in rng (fp mod p)

proof

let x be set ; :: thesis:
assume x in { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } ; :: thesis:
then ex k being Element of NAT st
( x = k & k in rng (fp mod p) & k > p / 2 ) ;
hence x in rng (fp mod p) ; :: thesis:

end;

then A10: { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } c= rng (fp mod p) by TARSKI:def 3;
then reconsider X = { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } as finite set ;
card X is Element of NAT ;
then reconsider m = card { k where k is Element of NAT : ( k in rng (fp mod p) & k > p / 2 ) } as Element of NAT ;
A11: len (fp mod p) = len fp by EULER_2:def 1;
then A12: dom (fp mod p) = dom fp by FINSEQ_3:31;
assume A13: p > 2 ; :: thesis:
then 2,p are_relative_prime by EULER_1:3;
then A14: 2 gcd p = 1 by INT_2:def 4;
then A15: Lege 2,p = (- 1) |^ m by A13, Th41;
not p is even by A13, PEPIN:17;
then A16: p - 1 is even by HILBERT3:2;
then A17: (p -' 1) div 2 = ((p -' 1) + 1) div 2 by A2, NAT_2:28
.= p div 2 by A1, XREAL_1:237 ;
then A18: fp mod p <> {} by A13, A6, A11, NAT_2:15;
then reconsider U = dom (fp mod p) as non empty finite Subset of NAT ;
2 divides p -' 1 by A16, A2, PEPIN:22;
then A19: p -' 1 = 2 * ((p -' 1) div 2) by NAT_D:3;
A20: for d being Nat st d in dom (fp mod p) holds
(fp mod p) . d = 2 * d

proof

let d be Nat; :: thesis:
assume A21: d in dom (fp mod p) ; :: thesis:
then d <= (p -' 1) div 2 by A6, A11, FINSEQ_3:27;
then 2 * d <= p -' 1 by A19, XREAL_1:66;
then 2 * d < p by NAT_2:11, XXREAL_0:2;
hence 2 * d = (2 * d) mod p by NAT_D:24
.= (fp . d) mod p by A3, A12, A21
.= (fp mod p) . d by A12, A21, EULER_2:def 1 ;
:: thesis:

end;

A22: for d1, d2, k1, k2 being Nat st 1 <= d1 & d1 < d2 & d2 <= len (fp mod p) & k1 = (fp mod p) . d1 & k2 = (fp mod p) . d2 holds
k1 < k2

proof

let d1, d2, k1, k2 be Nat; :: thesis:
assume that
A23: 1 <= d1 and
A24: d1 < d2 and
A25: d2 <= len (fp mod p) and
A26: k1 = (fp mod p) . d1 and
A27: k2 = (fp mod p) . d2 ; :: thesis:
1 <= d2 by A23, A24, XXREAL_0:2;
then d2 in dom (fp mod p) by A25, FINSEQ_3:27;
then A28: k2 = 2 * d2 by A20, A27;
d1 <= len (fp mod p) by A24, A25, XXREAL_0:2;
then d1 in dom (fp mod p) by A23, FINSEQ_3:27;
then k1 = 2 * d1 by A20, A26;
hence k1 < k2 by A24, A28, XREAL_1:70; :: thesis:

end;

rng (fp mod p) is non empty Subset of NAT by A18, FINSEQ_1:def 4;
then consider n1 being Element of NAT such that
A29: rng (fp mod p) c= (Seg n1) \/ {0 } by HEYTING3:3;
rng (fp mod p) c= NAT by FINSEQ_1:def 4;
then reconsider X = X as finite Subset of NAT by A10, XBOOLE_1:1;
seq (p div 4),(((p -' 1) div 2) -' (p div 4)),((p -' 1) div 2) -' (p div 4) are_equipotent by CALCUL_2:6;
then A30: card (seq (p div 4),(((p -' 1) div 2) -' (p div 4))) = card (((p -' 1) div 2) -' (p div 4)) by CARD_1:21
.= ((p -' 1) div 2) -' (p div 4) by CARD_1:def 5 ;
not 0 in rng (fp mod p)

proof

assume 0 in rng (fp mod p) ; :: thesis:
then consider n being Nat such that
A31: n in dom (fp mod p) and
A32: (fp mod p) . n = 0 by FINSEQ_2:11;
2 * n = 0 by A20, A31, A32;
hence contradiction by A31, FINSEQ_3:27; :: thesis:

end;

then A33: {0 } misses rng (fp mod p) by ZFMISC_1:56;
then rng (fp mod p) c= Seg n1 by A29, XBOOLE_1:73;
then A34: Sgm (rng (fp mod p)) = fp mod p by A22, FINSEQ_1:def 13;
A35: X,Y are_equipotent

proof

deffunc H₁( Element of U) -> set = (fp mod p) . $1;
set YY = { d where d is Element of U : H₁(d) in X } ;

A36: now

let x be set ; :: thesis:
assume x in X ; :: thesis:
then consider y being Element of NAT such that
A37: y = x and
A38: y in rng (fp mod p) and
y > p / 2 ;
consider d being Nat such that
A39: d in U and
A40: (fp mod p) . d = y by A38, FINSEQ_2:11;
reconsider d = d as Element of U by A39;
take d = d; :: thesis:
thus x = H₁(d) by A37, A40; :: thesis:

end;

A41: Y c= { d where d is Element of U : H₁(d) in X }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Y ; :: thesis:
then A42: ex d being Element of NAT st
( d = x & d in dom (fp mod p) & (fp mod p) . d > p / 2 ) ;
then reconsider x = x as Element of U ;
reconsider f = fp mod p as FinSequence of NAT ;
f . x in rng f by FUNCT_1:12;
then H₁(x) in X by A42;
hence x in { d where d is Element of U : H₁(d) in X } ; :: thesis:

end;

now

let x be set ; :: thesis:
assume x in { d where d is Element of U : H₁(d) in X } ; :: thesis:
then consider d being Element of U such that
A43: d = x and
A44: (fp mod p) . d in X ;
ex k being Element of NAT st
( k = (fp mod p) . d & k in rng (fp mod p) & k > p / 2 ) by A44;
hence x in Y by A43; :: thesis:

end;

then A45: { d where d is Element of U : H₁(d) in X } c= Y by TARSKI:def 3;
A46: for d1, d2 being Element of U st H₁(d1) = H₁(d2) holds
d1 = d2

proof

let d1, d2 be Element of U; :: thesis:
assume A47: H₁(d1) = H₁(d2) ; :: thesis:
fp mod p is one-to-one by A29, A33, A34, FINSEQ_3:99, XBOOLE_1:73;
hence d1 = d2 by A47, FUNCT_1:def 8; :: thesis:

end;

X,{ d where d is Element of U : H₁(d) in X } are_equipotent from FUNCT_7:sch 3(A36, A46);
hence X,Y are_equipotent by A41, A45, XBOOLE_0:def 10; :: thesis:

end;

p div 2 < p by INT_1:83;
then (p div 2) div 2 <= p div 2 by NAT_2:26;
then A48: p div (2 * 2) <= p div 2 by NAT_2:29;
A49: seq (p div 4),(((p -' 1) div 2) -' (p div 4)) c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A50: x in seq (p div 4),(((p -' 1) div 2) -' (p div 4)) ; :: thesis:
then reconsider x = x as Element of NAT ;
A51: x >= (p div 4) + 1 by A50, CALCUL_2:1;
then (p div 4) + x >= (p div 4) + 1 by NAT_1:12;
then A52: x >= 1 by XREAL_1:8;
x <= (((p -' 1) div 2) -' (p div 4)) + (p div 4) by A50, CALCUL_2:1;
then x <= (p -' 1) div 2 by A17, A48, XREAL_1:237;
then A53: x in dom (fp mod p) by A6, A11, A52, FINSEQ_3:27;
x > p / 4 by A51, INT_1:52, XXREAL_0:2;
then 2 * x > 2 * (p / 4) by XREAL_1:70;
then (fp mod p) . x > p / 2 by A20, A53;
hence x in Y by A53; :: thesis:

end;

now

let x be set ; :: thesis:
A54: p / 4 >= [\(p / 4)/] by INT_1:def 4;
assume x in Y ; :: thesis:
then consider x1 being Element of NAT such that
A55: x1 = x and
A56: x1 in dom (fp mod p) and
A57: (fp mod p) . x1 > p / 2 ;
2 * x1 > p / 2 by A20, A56, A57;
then x1 > (p / 2) / 2 by XREAL_1:85;
then x1 > [\(p / 4)/] by A54, XXREAL_0:2;
then A58: x1 >= (p div 4) + 1 by NAT_1:13;
x1 <= (p -' 1) div 2 by A6, A11, A56, FINSEQ_3:27;
then x1 <= (((p -' 1) div 2) -' (p div 4)) + (p div 4) by A17, A48, XREAL_1:237;
hence x in seq (p div 4),(((p -' 1) div 2) -' (p div 4)) by A55, A58; :: thesis:

end;

then Y c= seq (p div 4),(((p -' 1) div 2) -' (p div 4)) by TARSKI:def 3;
then Y = seq (p div 4),(((p -' 1) div 2) -' (p div 4)) by A49, XBOOLE_0:def 10;
then A59: m = ((p -' 1) div 2) -' (p div 4) by A30, A35, CARD_1:21;

A60: now

assume p mod 8 = 2 ; :: thesis:
then 8 divides p - 2 by PEPIN:8;
then 2 divides p - 2 by A8, INT_2:13;
then 2 divides - (p - 2) by INT_2:14;
then 2 divides 2 - p ;
then 2 divides p by Th2;
hence contradiction by A13, NAT_4:12; :: thesis:

end;

A61: now

assume p mod 8 = 4 ; :: thesis:
then 8 divides p - 4 by PEPIN:8;
then 2 divides p - 4 by A8, INT_2:13;
then 2 divides - (p - 4) by INT_2:14;
then A62: 2 divides 4 - p ;
4 = 2 * 2 ;
then 2 divides 4 by NAT_D:def 3;
then 2 divides p by A62, Th2;
hence contradiction by A13, NAT_4:12; :: thesis:

end;

A63: now

assume p mod 8 = 6 ; :: thesis:
then 8 divides p - 6 by PEPIN:8;
then 2 divides p - 6 by A8, INT_2:13;
then 2 divides - (p - 6) by INT_2:14;
then A64: 2 divides 6 - p ;
6 = 2 * 3 ;
then 2 divides 6 by NAT_D:def 3;
then 2 divides p by A64, Th2;
hence contradiction by A13, NAT_4:12; :: thesis:

end;

per cases by A9, A60, A61, A63, A7, NAT_1:32;

suppose p mod 8 = 1 ; :: thesis:

then A65: p = (8 * (p div 8)) + 1 by NAT_D:2;
then p -' 1 = 2 * (4 * (p div 8)) by A2;
then A66: (p -' 1) div 2 = 4 * (p div 8) by NAT_D:18;
p div 4 = ((4 * (2 * (p div 8))) + 1) div 4 by A65
.= (2 * (p div 8)) + (1 div 4) by INT_3:8
.= (2 * (p div 8)) + 0 by NAT_D:27 ;
then m = (4 * (p div 8)) - (2 * (p div 8)) by A59, A66, XREAL_1:66, XREAL_1:235
.= 2 * (p div 8) ;
then A67: Lege 2,p = ((- 1) |^ 2) |^ (p div 8) by A15, NEWTON:14
.= (1 |^ 2) |^ (p div 8) by WSIERP_1:2
.= (1 ^2 ) |^ (p div 8) by NEWTON:100
.= 1 by NEWTON:15 ;
((p ^2 ) -' 1) div 8 = (((((8 * (p div 8)) ^2 ) + (2 * (8 * (p div 8)))) + 1) -' 1) div 8 by A65
.= (8 * ((8 * ((p div 8) ^2 )) + (2 * (p div 8)))) div 8 by NAT_D:34
.= (8 * ((p div 8) ^2 )) + (2 * (p div 8)) by NAT_D:18 ;
hence (- 1) |^ (((p ^2 ) -' 1) div 8) = (- 1) |^ (2 * ((4 * ((p div 8) ^2 )) + (p div 8)))
.= ((- 1) |^ 2) |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by NEWTON:14
.= (1 |^ 2) |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by WSIERP_1:2
.= 1 |^ ((4 * ((p div 8) ^2 )) + (p div 8)) by NEWTON:15
.= Lege 2,p by A67, NEWTON:15 ;
:: thesis:

end;

suppose p mod 8 = 3 ; :: thesis:

then A68: p = (8 * (p div 8)) + 3 by NAT_D:2;
then p -' 1 = 2 * ((4 * (p div 8)) + 1) by A2;
then A69: (p -' 1) div 2 = (4 * (p div 8)) + 1 by NAT_D:18;
A70: 4 * (p div 8) >= 2 * (p div 8) by XREAL_1:66;
p div 4 = ((4 * (2 * (p div 8))) + 3) div 4 by A68
.= (2 * (p div 8)) + (3 div 4) by INT_3:8
.= (2 * (p div 8)) + 0 by NAT_D:27 ;
then m = ((4 * (p div 8)) + 1) - (2 * (p div 8)) by A59, A69, A70, NAT_1:12, XREAL_1:235
.= (2 * (p div 8)) + 1 ;
then A71: Lege 2,p = ((- 1) |^ (2 * (p div 8))) * (- 1) by A15, NEWTON:11
.= (((- 1) |^ 2) |^ (p div 8)) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ (p div 8)) * (- 1) by WSIERP_1:2
.= (1 |^ (p div 8)) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= - 1 ;
((p ^2 ) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2 ))) + (8 * (6 * (p div 8)))) + (3 * 3)) - 1) div 8 by A68, NAT_1:12, XREAL_1:235
.= (8 * (((8 * ((p div 8) ^2 )) + (6 * (p div 8))) + 1)) div 8
.= ((8 * ((p div 8) ^2 )) + (6 * (p div 8))) + 1 by NAT_D:18 ;
hence (- 1) |^ (((p ^2 ) -' 1) div 8) = ((- 1) |^ (2 * ((4 * ((p div 8) ^2 )) + (3 * (p div 8))))) * (- 1) by NEWTON:11
.= (((- 1) |^ 2) |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by WSIERP_1:2
.= (1 |^ ((4 * ((p div 8) ^2 )) + (3 * (p div 8)))) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= Lege 2,p by A71 ;
:: thesis:

end;

suppose p mod 8 = 5 ; :: thesis:

then A72: p = (8 * (p div 8)) + 5 by NAT_D:2;
then p -' 1 = 2 * ((4 * (p div 8)) + 2) by A2;
then A73: (p -' 1) div 2 = (4 * (p div 8)) + 2 by NAT_D:18;
A74: 4 * (p div 8) >= 2 * (p div 8) by XREAL_1:66;
p div 4 = ((4 * ((2 * (p div 8)) + 1)) + 1) div 4 by A72
.= ((2 * (p div 8)) + 1) + (1 div 4) by INT_3:8
.= ((2 * (p div 8)) + 1) + 0 by NAT_D:27 ;
then m = ((4 * (p div 8)) + 2) - ((2 * (p div 8)) + 1) by A59, A73, A74, XREAL_1:9, XREAL_1:235
.= (2 * (p div 8)) + 1 ;
then A75: Lege 2,p = ((- 1) |^ (2 * (p div 8))) * (- 1) by A15, NEWTON:11
.= (((- 1) |^ 2) |^ (p div 8)) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ (p div 8)) * (- 1) by WSIERP_1:2
.= (1 |^ (p div 8)) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= - 1 ;
((p ^2 ) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2 ))) + (8 * (10 * (p div 8)))) + 25) - 1) div 8 by A72, NAT_1:12, XREAL_1:235
.= (8 * (((8 * ((p div 8) ^2 )) + (10 * (p div 8))) + 3)) div 8
.= ((8 * ((p div 8) ^2 )) + (10 * (p div 8))) + 3 by NAT_D:18 ;
hence (- 1) |^ (((p ^2 ) -' 1) div 8) = (- 1) |^ ((((2 * (4 * ((p div 8) ^2 ))) + (2 * (5 * (p div 8)))) + (2 * 1)) + 1)
.= ((- 1) |^ (2 * (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1))) * (- 1) by NEWTON:11
.= (((- 1) |^ 2) |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:14
.= ((1 |^ 2) |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by WSIERP_1:2
.= (1 |^ (((4 * ((p div 8) ^2 )) + (5 * (p div 8))) + 1)) * (- 1) by NEWTON:15
.= 1 * (- 1) by NEWTON:15
.= Lege 2,p by A75 ;
:: thesis:

end;

suppose p mod 8 = 7 ; :: thesis:

then A76: p = (8 * (p div 8)) + 7 by NAT_D:2;
then p -' 1 = 2 * ((4 * (p div 8)) + 3) by A2;
then A77: (p -' 1) div 2 = (4 * (p div 8)) + 3 by NAT_D:18;
A78: 4 * (p div 8) >= 2 * (p div 8) by XREAL_1:66;
p div 4 = ((4 * ((2 * (p div 8)) + 1)) + 3) div 4 by A76
.= ((2 * (p div 8)) + 1) + (3 div 4) by INT_3:8
.= ((2 * (p div 8)) + 1) + 0 by NAT_D:27 ;
then m = ((4 * (p div 8)) + 3) - ((2 * (p div 8)) + 1) by A59, A77, A78, XREAL_1:9, XREAL_1:235
.= (2 * (p div 8)) + 2 ;
then A79: Lege 2,p = (- 1) |^ (2 * ((p div 8) + 1)) by A13, A14, Th41
.= ((- 1) |^ 2) |^ ((p div 8) + 1) by NEWTON:14
.= (1 |^ 2) |^ ((p div 8) + 1) by WSIERP_1:2
.= 1 |^ ((p div 8) + 1) by NEWTON:15
.= 1 by NEWTON:15 ;
((p ^2 ) -' 1) div 8 = ((((8 * (8 * ((p div 8) ^2 ))) + (8 * (14 * (p div 8)))) + 49) - 1) div 8 by A76, NAT_1:12, XREAL_1:235
.= (8 * (((8 * ((p div 8) ^2 )) + (14 * (p div 8))) + 6)) div 8
.= ((8 * ((p div 8) ^2 )) + (14 * (p div 8))) + 6 by NAT_D:18 ;
hence (- 1) |^ (((p ^2 ) -' 1) div 8) = (- 1) |^ (2 * (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3))
.= ((- 1) |^ 2) |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by NEWTON:14
.= (1 |^ 2) |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by WSIERP_1:2
.= 1 |^ (((4 * ((p div 8) ^2 )) + (7 * (p div 8))) + 3) by NEWTON:15
.= Lege 2,p by A79, NEWTON:15 ;
:: thesis:

end;